src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 tuned -- more explicit use of context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-09-08 blanchet 2014-09-08 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-01 blanchet 2014-09-01 tuned signatures
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place