src/HOL/Tools/Datatype/datatype.ML
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};
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;