| Tue, 24 Nov 2009 14:37:23 +0100 |
haftmann |
backported parts of abstract byte code verifier from AFP/Jinja
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 16:17:55 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:18:57 +0200 |
haftmann |
explicit Set constructor for code generated for sets
|
file |
diff |
annotate
|
| Mon, 18 May 2009 23:15:38 +0200 |
nipkow |
fine-tuned elimination of comprehensions involving x=t.
|
file |
diff |
annotate
|
| Sat, 16 May 2009 17:44:11 +0200 |
nipkow |
proof tuned
|
file |
diff |
annotate
|
| Sat, 16 May 2009 11:28:02 +0200 |
nipkow |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:25 +0200 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:54:51 +0200 |
wenzelm |
theory header: fixed import;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 17:46:31 +0200 |
wenzelm |
theory header: more precise imports;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:32:02 +0200 |
berghofe |
- Renamed inductive2 to inductive
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:26 +0200 |
haftmann |
added qualification for ambiguous definition names
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:44:07 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:56 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 09:17:21 +0200 |
haftmann |
removed quote in serialization
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:52 +0200 |
haftmann |
added some stuff for code generation 2
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 20:15:29 +0200 |
berghofe |
Now uses set implementation from ExecutableSet.
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2005 16:13:09 +0200 |
berghofe |
Adapted to new code generator syntax.
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 14:10:02 +0200 |
berghofe |
Added BasisLibrary prefix to List.concat to avoid problems with
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 13:11:34 +0200 |
nipkow |
Moved to new m<..<n syntax for set intervals.
|
file |
diff |
annotate
|
| Mon, 26 May 2003 18:36:15 +0200 |
streckem |
Introduced distinction wf_prog vs. ws_prog
|
file |
diff |
annotate
|
| Wed, 27 Nov 2002 17:11:38 +0100 |
berghofe |
Fixed bug in consts_code section.
|
file |
diff |
annotate
|
| Fri, 14 Jun 2002 23:25:36 +0200 |
kleing |
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
|
file |
diff |
annotate
|
| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Tue, 14 May 2002 12:33:42 +0200 |
kleing |
numerals work again
|
file |
diff |
annotate
|
| Sat, 11 May 2002 20:40:31 +0200 |
kleing |
fix for change in nat number simplification
|
file |
diff |
annotate
|
| Tue, 30 Apr 2002 13:00:29 +0200 |
kleing |
tuned
|
file |
diff |
annotate
|
| Fri, 19 Apr 2002 14:47:10 +0200 |
berghofe |
Added example for code generation.
|
file |
diff |
annotate
|
| Sat, 09 Mar 2002 20:39:46 +0100 |
kleing |
canonical start state
|
file |
diff |
annotate
|
| Thu, 07 Mar 2002 23:41:30 +0100 |
wenzelm |
renamed nat_number_of to nat_number (avoid clash with separate theorem);
|
file |
diff |
annotate
|
| Sun, 03 Mar 2002 16:59:08 +0100 |
kleing |
symbolized
|
file |
diff |
annotate
|
| Thu, 28 Feb 2002 13:38:49 +0100 |
kleing |
fixed document
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 15:45:32 +0100 |
kleing |
introduces SystemClasses and BVExample
|
file |
diff |
annotate
|