| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:15:33 +0100 |
wenzelm |
modernized functor/structures Interpretation;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:09:41 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 13:21:38 +0100 |
wenzelm |
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:55:27 +0100 |
wenzelm |
Datatype.read_typ: standard argument order;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 10:52:07 +0200 |
haftmann |
dropped Datatype.distinct_simproc
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 13 Oct 2009 14:08:01 +0200 |
haftmann |
deactivated Datatype.distinct_simproc
|
file |
diff |
annotate
|
| Tue, 13 Oct 2009 08:36:39 +0200 |
haftmann |
more appropriate abstraction over distinctness rules
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 15:26:40 +0200 |
haftmann |
dropped dist_ss
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 13:40:28 +0200 |
haftmann |
dropped rule duplicates
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 10:24:07 +0200 |
haftmann |
dropped redundancy
|
file |
diff |
annotate
|
| Fri, 09 Oct 2009 13:34:40 +0200 |
haftmann |
dropped simproc_dist formally
|
file |
diff |
annotate
|
| Thu, 08 Oct 2009 19:33:03 +0200 |
haftmann |
lookup for datatype constructors considers type annotations to resolve overloading
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 15:25:43 +0200 |
haftmann |
less auxiliary functions
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 14:54:15 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 14:48:30 +0200 |
haftmann |
shared code between rep_datatype and datatype
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 10:51:12 +0200 |
haftmann |
further unification of datatype and rep_datatype
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 10:20:21 +0200 |
haftmann |
avoid compound fields in datatype info record
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 09:47:18 +0200 |
haftmann |
explicit pointless checkpoint
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:58:25 +0200 |
haftmann |
emerging common infrastructure for datatype and rep_datatype
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:43:47 +0200 |
haftmann |
streamlined rep_datatype further
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:34:50 +0200 |
haftmann |
simplified rep_datatype
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:19:56 +0200 |
haftmann |
more appropriate order of field in dt_info
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:15:45 +0200 |
haftmann |
re-established reasonable inner outline for module
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 09:52:23 +0200 |
haftmann |
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
adapted configuration for DatatypeCase.make_case
|
file |
diff |
annotate
|
| Fri, 14 Aug 2009 15:36:57 +0200 |
haftmann |
inserted space into message
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 18:58:58 +0200 |
wenzelm |
renamed functor ProjectRuleFun to Project_Rule;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:52:30 +0200 |
haftmann |
dropped ancient flat_names option
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 16:17:56 +0200 |
haftmann |
canonical prefix for datatype derivates
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 15:32:34 +0200 |
haftmann |
add_datatypes does not yield particular rules any longer
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 14:50:34 +0200 |
haftmann |
add_datatype interface yields type names and less rules
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|