Fri, 30 Nov 2007 20:13:05 +0100 |
haftmann |
more canonical attribute application
|
file |
diff |
annotate
|
Thu, 04 Oct 2007 19:54:44 +0200 |
haftmann |
certificates for code generator case expressions
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
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:49:23 +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
|
Wed, 04 Apr 2007 00:10:59 +0200 |
wenzelm |
ML antiquotes;
|
file |
diff |
annotate
|
Mon, 12 Mar 2007 19:23:49 +0100 |
wenzelm |
syntax: proper body priorty for derived binders;
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:20 +0100 |
haftmann |
using "fst" "snd" for Haskell code
|
file |
diff |
annotate
|
Fri, 23 Feb 2007 08:39:22 +0100 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
Wed, 27 Dec 2006 19:09:57 +0100 |
haftmann |
moved code generator product setup here
|
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
|
Mon, 13 Nov 2006 15:43:08 +0100 |
haftmann |
added thy dependencies
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
Mon, 06 Nov 2006 16:28:36 +0100 |
haftmann |
two further lemmas on split
|
file |
diff |
annotate
|
Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:21:42 +0200 |
haftmann |
added operational equality
|
file |
diff |
annotate
|
Fri, 25 Aug 2006 18:45:57 +0200 |
paulson |
explicit type variables prevent empty sorts
|
file |
diff |
annotate
|
Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
Sat, 08 Jul 2006 12:54:30 +0200 |
wenzelm |
simprocs: no theory argument -- use simpset context instead;
|
file |
diff |
annotate
|
Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
Tue, 02 May 2006 20:42:30 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
Fri, 03 Mar 2006 19:30:20 +0100 |
nipkow |
changed and retracted change of location of code lemmas.
|
file |
diff |
annotate
|
Sat, 25 Feb 2006 15:19:47 +0100 |
haftmann |
improved codegen bootstrap
|
file |
diff |
annotate
|
Mon, 20 Feb 2006 11:38:06 +0100 |
haftmann |
slight code generator serialization improvements
|
file |
diff |
annotate
|