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