src/HOL/Tools/Datatype/datatype.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 avoid hard-wired theory names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
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
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-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
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-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
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;
2011-12-17 wenzelm 2011-12-17 eliminated Drule.export_without_context which is not really required here;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-16 wenzelm 2011-12-16 eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-12-15 wenzelm 2011-12-15 misc tuning and simplification;
2011-12-14 wenzelm 2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-14 wenzelm 2011-12-14 tuned;
2011-12-14 wenzelm 2011-12-14 tuned signature;
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-12-12 wenzelm 2011-12-12 datatype dtyp with explicit sort information; tuned messages;
2011-12-12 wenzelm 2011-12-12 tuned;
2011-12-02 wenzelm 2011-12-02 misc tuning;
2011-12-02 wenzelm 2011-12-02 some localization;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-12-02 wenzelm 2011-12-02 eliminated some legacy operations;
2011-12-02 wenzelm 2011-12-02 tuned signature;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-11-30 wenzelm 2011-11-30 misc tuning;
2011-10-21 wenzelm 2011-10-21 tuned;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2010-12-30 wenzelm 2010-12-30 do not open auxiliary ML structures;
2010-12-03 huffman 2010-12-03 theorem names generated by the (rep_)datatype command now have mandatory qualifiers
2010-11-26 wenzelm 2010-11-26 keep private things private, without comments;
2010-10-28 wenzelm 2010-10-28 preserve original source position of exn;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-15 wenzelm 2010-04-15 spelling;
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};