src/HOL/Tools/Datatype/datatype.ML
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