| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| Thu, 06 May 2004 12:43:00 +0200 |
tidied
|
file | diff | annotate |
| Wed, 24 Mar 2004 10:50:29 +0100 |
streamlined treatment of quotients for the integers
|
file | diff | annotate |
| Fri, 19 Mar 2004 10:44:20 +0100 |
stylistic tweaks
|
file | diff | annotate |
| Sun, 15 Feb 2004 10:46:37 +0100 |
Polymorphic treatment of binary arithmetic using axclasses
|
file | diff | annotate |
| Tue, 10 Feb 2004 12:02:11 +0100 |
generic of_nat and of_int functions, and generalization of iszero
|
file | diff | annotate |
| Tue, 27 Jan 2004 15:39:51 +0100 |
replacing HOL/Real/PRat, PNat by the rational number development
|
file | diff | annotate |
| Wed, 10 Dec 2003 15:59:34 +0100 |
Moving some theorems from Real/RealArith0.ML
|
file | diff | annotate |
| Sun, 07 Dec 2003 16:30:06 +0100 |
re-organisation of Real/RealArith0.ML; more `Isar scripts
|
file | diff | annotate |
| Fri, 05 Dec 2003 18:10:59 +0100 |
more field division lemmas transferred from Real to Ring_and_Field
|
file | diff | annotate |
| Thu, 04 Dec 2003 10:29:17 +0100 |
Tidying of the integer development; towards removing the
|
file | diff | annotate |
| Mon, 12 Aug 2002 17:48:19 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Mon, 22 Oct 2001 11:54:22 +0200 |
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 |
removed the mutual recursion from "bin_add"
|
file | diff | annotate |
| Tue, 13 Jul 1999 10:42:31 +0200 |
renamed sort "numeral" to "number"
|
file | diff | annotate |
| Tue, 06 Jul 1999 21:14:34 +0200 |
use generic numeral encoding and syntax;
|
file | diff | annotate |
| Wed, 17 Mar 1999 17:19:18 +0100 |
xnum token class;
|
file | diff | annotate |
| Tue, 29 Sep 1998 15:57:42 +0200 |
many renamings and changes. Simproc for cancelling common terms in relations
|
file | diff | annotate |
| Fri, 25 Sep 1998 13:57:01 +0200 |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file | diff | annotate |
| Thu, 24 Sep 1998 15:21:30 +0200 |
renamed some axioms
|
file | diff | annotate |
| Wed, 23 Sep 1998 10:25:37 +0200 |
much renaming and reorganization
|
file | diff | annotate |
| Mon, 21 Sep 1998 10:43:09 +0200 |
much renaming and tidying
|
file | diff | annotate |
| Fri, 18 Sep 1998 16:05:08 +0200 |
improved (but still flawed) treatment of binary arithmetic
|
file | diff | annotate |
| Tue, 15 Sep 1998 15:06:29 +0200 |
revised treatment of integers
|
file | diff | annotate |
| Fri, 24 Jul 1998 13:19:38 +0200 |
Adapted to new datatype package.
|
file | diff | annotate |
| Mon, 09 Mar 1998 16:16:21 +0100 |
Symbol.explode;
|
file | diff | annotate |
| Mon, 06 Oct 1997 19:15:22 +0200 |
eliminated raise_term;
|
file | diff | annotate |
| Fri, 18 Apr 1997 11:54:54 +0200 |
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
|
file | diff | annotate |
| Fri, 29 Mar 1996 13:18:26 +0100 |
Binary integers and their numeric syntax
|
file | diff | annotate |