| Thu, 21 Jun 2007 20:07:26 +0200 |
wenzelm |
tuned proofs -- avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 15 Jun 2007 19:19:23 +0200 |
berghofe |
Locally added definition of "int :: nat => int" again to make
|
file |
diff |
annotate
|
| Thu, 10 May 2007 15:51:59 +0200 |
berghofe |
Moved extraction_expand declaration of listall_def outside of definition.
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:22:17 +0200 |
haftmann |
consts in consts_code Isar commands are now referred to by usual term syntax
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
| Fri, 23 Mar 2007 12:06:41 +0100 |
haftmann |
fixed typing bug in generated code
|
file |
diff |
annotate
|
| Fri, 23 Mar 2007 12:05:43 +0100 |
haftmann |
fixed typing bug in generated code
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 14:03:30 +0100 |
haftmann |
fixed code generator setup
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:44:07 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:33 +0100 |
haftmann |
removed HOL structure
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:12 +0100 |
haftmann |
adjusted name in generated code
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:37 +0100 |
haftmann |
(adjustions)
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 16:52:46 +0200 |
haftmann |
added codegen2 example
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 10:34:42 +0200 |
haftmann |
purged some ML legacy
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:00:56 +0200 |
haftmann |
cleaned mess
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
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
|
| Wed, 14 Jun 2006 12:14:42 +0200 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 15:02:09 +0200 |
haftmann |
added arbitray setup for codegen 2
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 20:02:30 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 13:10:12 +0100 |
berghofe |
Factored out proof for normalization of applications (norm_list).
|
file |
diff |
annotate
|