| Fri, 22 Jan 2010 13:38:28 +0100 |
haftmann |
code literals: distinguish numeral classes by different entries
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 17:54:54 +0100 |
haftmann |
dedicated conversions to and from Int
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 17:47:39 +0100 |
haftmann |
added Scala setup
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 10:18:45 +0100 |
haftmann |
function transformer preprocessor applies to both code generators
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 22:16:40 +0100 |
haftmann |
adjusted to changes in theory Divides
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 10:49:08 +0200 |
haftmann |
repair mess produced by resolution afterwards
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 10:11:13 +0200 |
haftmann |
additional preprocessor rule
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:37:00 +0200 |
haftmann |
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 15:53:05 +0200 |
haftmann |
OCaml builtin intergers are elusive; avoid
|
file |
diff |
annotate
|
| Sat, 30 May 2009 08:16:44 +0200 |
haftmann |
corrected bound/unbounded flag for nat numerals
|
file |
diff |
annotate
|
| Tue, 19 May 2009 16:54:55 +0200 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:32 +0200 |
haftmann |
moved Code_Index, Random and Quickcheck before Main
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:38 +0200 |
haftmann |
adapted to changes in module Code
|
file |
diff |
annotate
|
| Mon, 11 May 2009 10:53:19 +0200 |
haftmann |
clarified matter of "proper" flag in code equations
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 19:11:16 +0100 |
haftmann |
faster preprocessor
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:38:09 +0100 |
haftmann |
dropped clause_suc_preproc for generic code generator
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 09:05:19 +0100 |
haftmann |
mandatory prefix for index conversion operations
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 19:37:00 +0100 |
haftmann |
changed name space policy for Haskell includes
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 13:36:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
eliminated OldTerm.(add_)term_consts;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 21:46:48 +0100 |
wenzelm |
canonical Term.add_var_names;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 08:47:45 -0800 |
huffman |
change more lemmas to avoid using iszero
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:15:49 +0100 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:35 +0200 |
haftmann |
more clever module name aliasses for code generation
|
file |
diff |
annotate
|