src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-24 wenzelm 2015-07-24 proper context;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-31 wenzelm 2015-03-31 tuned signature;
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-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
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-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place