| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:28 +0100 |
haftmann |
whitespace fix
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:45:31 +0100 |
haftmann |
introduced mk/dest_numeral/number for mk/dest_binum etc.
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:56 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:37 +0200 |
haftmann |
added normal post setup
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:52 +0200 |
wenzelm |
standardized facts;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2006 17:04:15 +0200 |
haftmann |
refinements in codegen serializer
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:58 +0200 |
haftmann |
improved numeral handling for nbe
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:05:50 +0200 |
krauss |
Major update to function package, including new syntax and the (only theoretical)
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Mon, 21 Aug 2006 11:02:41 +0200 |
haftmann |
more concise preprocessing of numerals for code generation
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:19:44 +0200 |
haftmann |
cleanup code generation for Numerals
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Tue, 09 May 2006 10:10:28 +0200 |
haftmann |
added codegen preprocessors for numerals
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:25:11 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 16 Jun 2005 19:51:04 +0200 |
paulson |
a few new integer lemmas
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Wed, 24 Mar 2004 10:50:29 +0100 |
paulson |
streamlined treatment of quotients for the integers
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:44:20 +0100 |
paulson |
stylistic tweaks
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:19:55 +0100 |
paulson |
some new results
|
file |
diff |
annotate
|