src/HOL/Library/old_recdef.ML
2016-01-05 wenzelm 2016-01-05 updated headers;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-10-17 wenzelm 2015-10-17 tuned signature;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-08-28 wenzelm 2015-08-28 tuned;
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-28 wenzelm 2015-07-28 more explicit context; tuned signature;
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-24 wenzelm 2015-07-24 proper context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-09 wenzelm 2015-07-09 clarified context; eliminated dead code;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-19 wenzelm 2015-06-19 removed dead code;
2015-06-19 wenzelm 2015-06-19 discontinued unused 'defer_recdef';
2015-06-19 wenzelm 2015-06-19 tuned;
2015-06-19 wenzelm 2015-06-19 removed dead code;
2015-06-19 wenzelm 2015-06-19 moved sources;