| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:16 +0200 |
haftmann |
hide names in theory Random
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:14:02 +0100 |
haftmann |
moved Random.thy to Library
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:23 +0200 |
haftmann |
more Isar for example
|
file |
diff |
annotate
|
| 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
|
| Fri, 25 Jan 2008 23:50:33 +0100 |
wenzelm |
modernized primrec;
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 10:53:39 +0100 |
berghofe |
Tuned.
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:49 +0200 |
haftmann |
renamed code_gen to export_code
|
file |
diff |
annotate
|
| Mon, 13 Aug 2007 21:22:37 +0200 |
haftmann |
renamed keyword "to" to "module_name"
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:10:02 +0200 |
haftmann |
code generator setup improved
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 09:29:03 +0200 |
haftmann |
dropped outer ROOT structure for generated code
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:16:34 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
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
|
| Wed, 07 Feb 2007 17:34:43 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:30 +0100 |
haftmann |
adjusted syntax for internal code generation
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:37 +0100 |
haftmann |
(adjustions)
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:38 +0100 |
haftmann |
added code gen II
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:57 +0100 |
haftmann |
disabled some code generation (an intermeidate solution)
|
file |
diff |
annotate
|
| 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
|