| 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
|
| Tue, 17 Feb 2004 10:41:59 +0100 |
paulson |
further tweaks to the numeric theories
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Mon, 15 Dec 2003 16:38:25 +0100 |
paulson |
more general lemmas for Ring_and_Field
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
file |
diff |
annotate
|
| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Thu, 06 Mar 2003 15:02:51 +0100 |
paulson |
new simprule for int (nat n)
|
file |
diff |
annotate
|
| Thu, 27 Feb 2003 18:22:49 +0100 |
paulson |
Reorganized, moving many results about the integer dvd relation from IntPrimes
|
file |
diff |
annotate
|
| Tue, 29 Oct 2002 11:32:52 +0100 |
nipkow |
added induction thms
|
file |
diff |
annotate
|
| Wed, 25 Sep 2002 07:42:24 +0200 |
nipkow |
added nat_split
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:33:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Sat, 01 Jul 2000 17:52:52 +0200 |
nipkow |
Defined abs on int.
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:48:23 +0200 |
wenzelm |
simprocs now in IntArith;
|
file |
diff |
annotate
|