src/HOL/Library/old_recdef.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;