src/HOL/Tools/Datatype/datatype.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-13 haftmann 2009-10-13 deactivated Datatype.distinct_simproc
2009-10-13 haftmann 2009-10-13 more appropriate abstraction over distinctness rules
2009-10-12 haftmann 2009-10-12 dropped dist_ss
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-08 haftmann 2009-10-08 lookup for datatype constructors considers type annotations to resolve overloading
2009-09-28 haftmann 2009-09-28 less auxiliary functions
2009-09-28 haftmann 2009-09-28 tuned
2009-09-28 haftmann 2009-09-28 shared code between rep_datatype and datatype
2009-09-28 haftmann 2009-09-28 further unification of datatype and rep_datatype
2009-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-28 haftmann 2009-09-28 explicit pointless checkpoint
2009-09-27 haftmann 2009-09-27 emerging common infrastructure for datatype and rep_datatype
2009-09-27 haftmann 2009-09-27 streamlined rep_datatype further
2009-09-27 haftmann 2009-09-27 simplified rep_datatype
2009-09-27 haftmann 2009-09-27 more appropriate order of field in dt_info
2009-09-27 haftmann 2009-09-27 re-established reasonable inner outline for module
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-09-23 bulwahn 2009-09-23 adapted configuration for DatatypeCase.make_case
2009-08-14 haftmann 2009-08-14 inserted space into message
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-06-29 haftmann 2009-06-29 canonical prefix for datatype derivates
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 add_datatypes does not yield particular rules any longer
2009-06-23 haftmann 2009-06-23 add_datatype interface yields type names and less rules
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories