src/HOL/Tools/Datatype/datatype.ML
Thu, 15 Apr 2010 15:38:58 +0200 wenzelm spelling;
Sat, 27 Mar 2010 21:38:38 +0100 wenzelm Typedef.info: separate global and local part, only the latter is transformed by morphisms;
Fri, 19 Mar 2010 00:47:23 +0100 wenzelm typedef etc.: no constraints;
Sat, 13 Mar 2010 14:43:04 +0100 wenzelm global typedef;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 28 Feb 2010 23:51:31 +0100 wenzelm more antiquotations;
Sat, 27 Feb 2010 20:57:08 +0100 wenzelm clarified @{const_name} vs. @{const_abbrev};
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Wed, 24 Feb 2010 20:37:01 +0100 wenzelm allow general mixfix syntax for type constructors;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Mon, 30 Nov 2009 12:28:12 +0100 haftmann dropped some unused bindings
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 27 Nov 2009 08:41:10 +0100 haftmann renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
Wed, 25 Nov 2009 11:16:57 +0100 haftmann bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 16:15:33 +0100 wenzelm modernized functor/structures Interpretation;
Thu, 29 Oct 2009 16:09:41 +0100 wenzelm tuned whitespace;
Thu, 29 Oct 2009 13:21:38 +0100 wenzelm separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
Tue, 27 Oct 2009 22:55:27 +0100 wenzelm Datatype.read_typ: standard argument order;
Thu, 22 Oct 2009 10:52:07 +0200 haftmann dropped Datatype.distinct_simproc
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 13 Oct 2009 14:08:01 +0200 haftmann deactivated Datatype.distinct_simproc
Tue, 13 Oct 2009 08:36:39 +0200 haftmann more appropriate abstraction over distinctness rules
Mon, 12 Oct 2009 15:26:40 +0200 haftmann dropped dist_ss
Mon, 12 Oct 2009 13:40:28 +0200 haftmann dropped rule duplicates
Mon, 12 Oct 2009 10:24:07 +0200 haftmann dropped redundancy
Fri, 09 Oct 2009 13:34:40 +0200 haftmann dropped simproc_dist formally
Thu, 08 Oct 2009 19:33:03 +0200 haftmann lookup for datatype constructors considers type annotations to resolve overloading
Mon, 28 Sep 2009 15:25:43 +0200 haftmann less auxiliary functions
Mon, 28 Sep 2009 14:54:15 +0200 haftmann tuned
Mon, 28 Sep 2009 14:48:30 +0200 haftmann shared code between rep_datatype and datatype
Mon, 28 Sep 2009 10:51:12 +0200 haftmann further unification of datatype and rep_datatype
Mon, 28 Sep 2009 10:20:21 +0200 haftmann avoid compound fields in datatype info record
Mon, 28 Sep 2009 09:47:18 +0200 haftmann explicit pointless checkpoint
Sun, 27 Sep 2009 20:58:25 +0200 haftmann emerging common infrastructure for datatype and rep_datatype
Sun, 27 Sep 2009 20:43:47 +0200 haftmann streamlined rep_datatype further
Sun, 27 Sep 2009 20:34:50 +0200 haftmann simplified rep_datatype
Sun, 27 Sep 2009 20:19:56 +0200 haftmann more appropriate order of field in dt_info
Sun, 27 Sep 2009 20:15:45 +0200 haftmann re-established reasonable inner outline for module
Sun, 27 Sep 2009 09:52:23 +0200 haftmann registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn adapted configuration for DatatypeCase.make_case
Fri, 14 Aug 2009 15:36:57 +0200 haftmann inserted space into message
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Tue, 21 Jul 2009 15:52:30 +0200 haftmann dropped ancient flat_names option
Mon, 29 Jun 2009 16:17:56 +0200 haftmann canonical prefix for datatype derivates
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Tue, 23 Jun 2009 15:32:34 +0200 haftmann add_datatypes does not yield particular rules any longer
Tue, 23 Jun 2009 14:50:34 +0200 haftmann add_datatype interface yields type names and less rules
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
less more (0) tip