src/HOL/Tools/Datatype/datatype_aux.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-02-25 ago more antiquotations;
2009-12-04 ago modernized structure Datatype_Aux
2009-12-02 ago tuned
2009-11-30 ago modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago Datatype.read_typ: standard argument order;
2009-10-27 ago normalized basic type abbreviations;
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-17 ago tuned signature;
2009-10-15 ago replaced String.concat by implode;
2009-10-09 ago dropped simproc_dist formally
2009-09-28 ago moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-28 ago avoid compound fields in datatype info record
2009-09-27 ago more appropriate order of field in dt_info
2009-09-27 ago registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-21 ago dropped ancient flat_names option
2009-06-23 ago uniformly capitialized names for subdirectories