| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 08:08:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 11:16:57 +0100 |
haftmann |
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 16:26:04 +0100 |
berghofe |
Streamlined setup for monotonicity rules (no longer requires classical rules).
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:43 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 12:03:47 +0200 |
haftmann |
stripped legacy ML bindings
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 13:43:05 +0200 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 14:19:13 +0200 |
haftmann |
moved Inductive.myinv to Fun.inv; tuned
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 15:04:33 +0200 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 20:31:36 +0100 |
wenzelm |
eliminated OldTerm.add_term_free_names;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:35 +0200 |
berghofe |
Instantiated some rules to avoid problems with HO unification.
|
file |
diff |
annotate
|
| Wed, 30 Jan 2008 10:57:44 +0100 |
haftmann |
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 15:10:09 +0100 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:03 +0100 |
haftmann |
adjustions to due to instance target
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 22:03:25 +0200 |
haftmann |
integrated FixedPoint into Inductive
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:54:46 +0200 |
haftmann |
tuned datatype_codegen setup
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 19:17:55 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:38 +0200 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:10:13 +0200 |
nipkow |
Final mods for list comprehension
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 10:59:23 +0200 |
berghofe |
Added new package for inductive sets.
|
file |
diff |
annotate
|