| Fri, 24 Nov 2006 13:43:44 +0100 |
krauss |
The function package declares the [code] attribute automatically again.
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 17:05:44 +0100 |
haftmann |
added filter_set; adaptions to more strict type discipline for code lemmas
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:42:58 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:01:59 +0100 |
krauss |
auto_term => lexicographic_order
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:39 +0100 |
haftmann |
adapted to changes in codegen_data.ML
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:29:01 +0100 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:42 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 09:02:21 +0200 |
haftmann |
explicit nonfix for union and inter
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 09:17:20 +0200 |
haftmann |
added code_abstype
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:00:58 +0200 |
haftmann |
added code for insert
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:22:05 +0200 |
haftmann |
code generation 2 adjustments
|
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
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| Wed, 14 Jun 2006 12:14:13 +0200 |
haftmann |
slight adaptions for code generator
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 15:02:55 +0200 |
haftmann |
refined code generation
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Sat, 25 Feb 2006 15:19:19 +0100 |
haftmann |
change in codegen syntax
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 17:09:25 +0100 |
haftmann |
some fixes
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 08:47:43 +0100 |
haftmann |
slight improvements in code generation
|
file |
diff |
annotate
|
| Mon, 30 Jan 2006 08:20:56 +0100 |
haftmann |
adaptions to codegen_package
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:44:39 +0100 |
wenzelm |
fixed code_generate syntax;
|
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
|
| Sun, 25 Sep 2005 20:12:26 +0200 |
berghofe |
New theory for implementing finite sets by lists.
|
file |
diff |
annotate
|