| Sun, 24 Aug 2008 14:42:24 +0200 |
haftmann |
default replaces arbitrary
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 10:55:08 +0100 |
berghofe |
Moved nat_eq_dec to Util.thy
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:49 +0200 |
haftmann |
renamed code_gen to export_code
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:30 +0100 |
haftmann |
adjusted syntax for internal code generation
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:52 +0200 |
haftmann |
added some stuff for code generation 2
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 16:05:42 +0200 |
nipkow |
rules -> iprover
|
file |
diff |
annotate
|
| Thu, 25 Aug 2005 16:13:09 +0200 |
berghofe |
Adapted to new code generator syntax.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 13 Oct 2004 07:40:13 +0200 |
nipkow |
mod becuase of chnage in induct
|
file |
diff |
annotate
|
| Mon, 28 Apr 2003 10:33:57 +0200 |
berghofe |
Converted main proof to Isar.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:44:42 +0200 |
berghofe |
Examples for program extraction in HOL.
|
file |
diff |
annotate
|