src/HOL/Tools/Datatype/rep_datatype.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-03-06 wenzelm 2014-03-06 more rigid const demands, based on educated guesses about the tools involved here;
2014-03-06 wenzelm 2014-03-06 eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-02-21 blanchet 2014-02-21 renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
2014-02-12 blanchet 2014-02-12 use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
2014-02-12 blanchet 2014-02-12 avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
2014-02-12 blanchet 2014-02-12 tuned code
2014-02-03 wenzelm 2014-02-03 more formal markup;
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-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
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-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-17 wenzelm 2011-12-17 clarified modules that contribute to datatype package;
2011-12-16 wenzelm 2011-12-16 eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;