| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:13 +0100 |
haftmann |
reduced verbosity
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:14 +0100 |
haftmann |
adapted seralizer syntax
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:54 +0100 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:27 +0200 |
haftmann |
added reserved words for Haskell
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:37 +0200 |
haftmann |
added normal post setup
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:01:14 +0200 |
haftmann |
clarified setup name
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:21 +0200 |
wenzelm |
merged with theory Datatype_Universe;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:20 +0200 |
wenzelm |
removed obsolete sum_case_Inl/Inr;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:42 +0200 |
haftmann |
added operational equality
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:05:50 +0200 |
krauss |
Major update to function package, including new syntax and the (only theoretical)
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
| Wed, 14 Jun 2006 12:14:42 +0200 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 16:55:14 +0200 |
haftmann |
slight code generator cleanup
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 14:56:42 +0200 |
haftmann |
improved code lemmas
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 14:26:07 +0200 |
krauss |
HOL/Tools/function_package: Added support for mutual recursive definitions.
|
file |
diff |
annotate
|
| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:11:30 +0200 |
haftmann |
adapted for definitional code generation
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 14:09:48 +0100 |
haftmann |
substantial improvement in codegen iml
|
file |
diff |
annotate
|
| Fri, 03 Mar 2006 19:30:20 +0100 |
nipkow |
changed and retracted change of location of code lemmas.
|
file |
diff |
annotate
|
| Mon, 27 Feb 2006 15:51:37 +0100 |
haftmann |
class package and codegen refinements
|
file |
diff |
annotate
|
| Sat, 25 Feb 2006 15:19:47 +0100 |
haftmann |
improved codegen bootstrap
|
file |
diff |
annotate
|
| Mon, 20 Feb 2006 11:38:06 +0100 |
haftmann |
slight code generator serialization improvements
|
file |
diff |
annotate
|
| Mon, 23 Jan 2006 14:07:52 +0100 |
haftmann |
removed problematic keyword 'atom'
|
file |
diff |
annotate
|
| Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|