| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Sun, 07 Dec 2003 16:30:06 +0100 |
paulson |
re-organisation of Real/RealArith0.ML; more `Isar scripts
|
file |
diff |
annotate
|
| Fri, 05 Dec 2003 18:10:59 +0100 |
paulson |
more field division lemmas transferred from Real to 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
|
| Mon, 12 Aug 2002 17:48:19 +0200 |
nipkow |
*** empty log message ***
|
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, 30 Jun 2000 10:59:50 +0200 |
paulson |
removed the mutual recursion from "bin_add"
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:42:31 +0200 |
paulson |
renamed sort "numeral" to "number"
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:14:34 +0200 |
wenzelm |
use generic numeral encoding and syntax;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 17:19:18 +0100 |
wenzelm |
xnum token class;
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:57:42 +0200 |
paulson |
many renamings and changes. Simproc for cancelling common terms in relations
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:57:01 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 15:21:30 +0200 |
paulson |
renamed some axioms
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:25:37 +0200 |
paulson |
much renaming and reorganization
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 10:43:09 +0200 |
paulson |
much renaming and tidying
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:05:08 +0200 |
paulson |
improved (but still flawed) treatment of binary arithmetic
|
file |
diff |
annotate
|
| Tue, 15 Sep 1998 15:06:29 +0200 |
paulson |
revised treatment of integers
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:16:21 +0100 |
wenzelm |
Symbol.explode;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 19:15:22 +0200 |
wenzelm |
eliminated raise_term;
|
file |
diff |
annotate
|
| Fri, 18 Apr 1997 11:54:54 +0200 |
paulson |
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
|
file |
diff |
annotate
|
| Fri, 29 Mar 1996 13:18:26 +0100 |
paulson |
Binary integers and their numeric syntax
|
file |
diff |
annotate
|