src/HOL/Tools/Datatype/datatype.ML
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-05 haftmann 2010-05-05 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-04-15 wenzelm 2010-04-15 spelling;
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 modernized functor/structures Interpretation;
2009-10-29 wenzelm 2009-10-29 tuned whitespace;
2009-10-29 wenzelm 2009-10-29 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-22 haftmann 2009-10-22 dropped Datatype.distinct_simproc
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
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