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