Mon, 02 Oct 2006 23:00:53 +0200 |
haftmann |
added example for code_gen
|
file |
diff |
annotate
|
Wed, 20 Sep 2006 10:13:36 +0200 |
haftmann |
removed debug
|
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
|
Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
Wed, 07 May 2003 16:58:17 +0200 |
berghofe |
Some tuning:
|
file |
diff |
annotate
|
Mon, 28 Apr 2003 10:33:42 +0200 |
berghofe |
Converted main proofs to Isar.
|
file |
diff |
annotate
|
Wed, 13 Nov 2002 15:34:01 +0100 |
berghofe |
Removed (now unneeded) declarations of realizers for bar induction.
|
file |
diff |
annotate
|
Wed, 07 Aug 2002 16:49:25 +0200 |
berghofe |
Removed (now unneeded) declarations of realizers for induction on lists and letters.
|
file |
diff |
annotate
|
Sun, 21 Jul 2002 15:44:42 +0200 |
berghofe |
Examples for program extraction in HOL.
|
file |
diff |
annotate
|