| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
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 |
| Fri, 05 Mar 2004 15:19:55 +0100 |
some new results
|
file | diff | annotate |
| Tue, 17 Feb 2004 10:41:59 +0100 |
further tweaks to the numeric theories
|
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 |
| Mon, 12 Jan 2004 16:51:45 +0100 |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file | diff | annotate |
| Mon, 15 Dec 2003 16:38:25 +0100 |
more general lemmas for 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 |
| Wed, 03 Dec 2003 10:49:34 +0100 |
Simplification of the development of Integers
|
file | diff | annotate |
| Mon, 24 Nov 2003 15:33:07 +0100 |
conversion of integers to use Ring_and_Field;
|
file | diff | annotate |
| Tue, 18 Nov 2003 11:01:52 +0100 |
conversion of ML to Isar scripts
|
file | diff | annotate |
| Thu, 06 Mar 2003 15:02:51 +0100 |
new simprule for int (nat n)
|
file | diff | annotate |
| Thu, 27 Feb 2003 18:22:49 +0100 |
Reorganized, moving many results about the integer dvd relation from IntPrimes
|
file | diff | annotate |
| Tue, 29 Oct 2002 11:32:52 +0100 |
added induction thms
|
file | diff | annotate |
| Wed, 25 Sep 2002 07:42:24 +0200 |
added nat_split
|
file | diff | annotate |
| Sat, 03 Nov 2001 01:33:54 +0100 |
tuned;
|
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, 01 Dec 2000 19:53:29 +0100 |
Linear arithmetic now copes with mixed nat/int formulae.
|
file | diff | annotate |
| Tue, 25 Jul 2000 00:06:46 +0200 |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file | diff | annotate |
| Sat, 01 Jul 2000 17:52:52 +0200 |
Defined abs on int.
|
file | diff | annotate |
| Mon, 04 Oct 1999 21:48:23 +0200 |
simprocs now in IntArith;
|
file | diff | annotate |