| Thu, 10 May 2007 15:49:31 +0200 |
berghofe |
Name of ML function "not" is now qualified in order to avoid
|
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
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
file |
diff |
annotate
|
| Wed, 09 May 2007 07:53:06 +0200 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 17:58:24 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 14:03:30 +0100 |
haftmann |
fixed code generator setup
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 17:07:23 +0100 |
krauss |
simplified "eval" oracle method
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:37 +0100 |
haftmann |
switched exception from arbitrary to undefined
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:53 +0100 |
haftmann |
dropped code datatype certificates
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:16 +0100 |
haftmann |
syntax for "class attach const"
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:06 +0100 |
wenzelm |
simplified ML setup;
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 20:00:59 +0100 |
haftmann |
fixed eval oracle
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 20:34:17 +0100 |
haftmann |
changed syntax for axclass attach
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:09:53 +0100 |
haftmann |
moved code generator bool setup here
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:25 +0100 |
haftmann |
new-style oracle setup
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:46 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:33 +0100 |
haftmann |
removed HOL structure
|
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:37 +0100 |
haftmann |
added evaluation oracle
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:35 +0100 |
haftmann |
dropped equals_conv for nbe
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:53 +0100 |
haftmann |
adaptions to changes in preprocessor
|
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:36 +0200 |
haftmann |
added if_delayed
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|