| Tue, 10 Feb 2004 12:02:11 +0100 |
generic of_nat and of_int functions, and generalization of iszero
|
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 |
| Wed, 03 Dec 2003 10:49:34 +0100 |
Simplification of the development of Integers
|
file | diff | annotate |
| Fri, 29 Aug 2003 15:19:02 +0200 |
Methods rule_tac etc support static (Isar) contexts.
|
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 |
| Wed, 26 Feb 2003 13:16:07 +0100 |
zprime_def fixes by Jeremy Avigad
|
file | diff | annotate |
| Tue, 28 Jan 2003 07:39:29 +0100 |
pos/neg_mod_sign/bound are now simp rules.
|
file | diff | annotate |
| Tue, 08 Oct 2002 08:20:17 +0200 |
Got rid of rotates because of new simplifier
|
file | diff | annotate |
| Mon, 30 Sep 2002 16:14:02 +0200 |
Adapted to new simplifier.
|
file | diff | annotate |
| Tue, 27 Aug 2002 11:03:05 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 23 Aug 2002 07:41:05 +0200 |
Added div+mod cancelling simproc
|
file | diff | annotate |
| Fri, 31 May 2002 12:27:24 +0200 |
finished an incomplete proof
|
file | diff | annotate |
| Thu, 30 May 2002 10:12:52 +0200 |
Modifications due to enhanced linear arithmetic.
|
file | diff | annotate |
| Tue, 28 May 2002 11:06:06 +0200 |
conversion of IntDiv.thy to Isar format
|
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, 05 Oct 2001 21:52:39 +0200 |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file | diff | annotate |
| Sun, 04 Feb 2001 19:31:13 +0100 |
HOL-NumberTheory: converted to new-style format and proper document setup;
|
file | diff | annotate |
| Tue, 03 Oct 2000 22:37:16 +0200 |
tuned deps;
|
file | diff | annotate |
| Wed, 13 Sep 2000 18:46:09 +0200 |
zgcd now works for negative integers
|
file | diff | annotate |
| Thu, 03 Aug 2000 10:46:01 +0200 |
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
|
file | diff | annotate |