src/HOL/Nominal/nominal_datatype.ML
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-05-30 wenzelm 2016-05-30 allow 'for' fixes for multi_specs;
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-03 wenzelm 2015-09-03 more general Typedef.bindings; tuned signature;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate; clarified context;
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-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-02 wenzelm 2015-06-02 clarified context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-04-10 blanchet 2015-04-10 renamed ML funs
2015-04-09 wenzelm 2015-04-09 make SML/NJ more happy;
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 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 misc tuning;
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-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 proof context for typedef;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-11 blanchet 2014-09-11 speed up old Nominal by killing type variables
2014-09-08 blanchet 2014-09-08 added flag to 'typedef' to allow concealed definitions
2014-09-08 blanchet 2014-09-08 ported old Nominal to use new datatypes
2014-09-08 blanchet 2014-09-08 use compatibility layer
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-01-01 wenzelm 2014-01-01 clarified simplifier context; eliminated Simplifier.global_context;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-10 wenzelm 2013-04-10 formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;
2013-02-14 wenzelm 2013-02-14 more parallel proofs in 'nominal_datatype', although sequential dark matter remains;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-09-05 wenzelm 2012-09-05 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2012-01-09 wenzelm 2012-01-09 prefer antiquotations;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-16 wenzelm 2011-12-16 tuned signature;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-12-15 wenzelm 2011-12-15 misc tuning and simplification;