src/HOL/Nominal/nominal_datatype.ML
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
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-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-27 wenzelm 2010-04-27 really minimize sorts after certification -- looks like this is intended here;
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
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-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
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 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-17 wenzelm 2009-11-17 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-25 wenzelm 2009-10-25 name space groups are identified by serial, not serial_string;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-27 haftmann 2009-09-27 adjusted to changes in datatype package
2009-07-26 wenzelm 2009-07-26 SUBPROOF/Obtain.result: named params;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union
2009-07-22 haftmann 2009-07-22 explicit antiquotation
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML