src/HOL/Tools/Datatype/datatype_rep_proofs.ML
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
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-10-29 wenzelm 2009-10-29 eliminated some old folds;
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 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-19 berghofe 2009-10-19 Replaced inv by the_inv_onto.
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-12 haftmann 2009-10-12 dropped rule duplicates
2009-10-12 haftmann 2009-10-12 dropped redundancy
2009-10-09 haftmann 2009-10-09 dropped simproc_dist formally
2009-10-05 haftmann 2009-10-05 experimental de-facto abolishment of distinctness limit
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-06 haftmann 2009-07-06 moved Inductive.myinv to Fun.inv; tuned
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories