| Thu, 26 Apr 2007 13:33:07 +0200 |
haftmann |
replaced recdef by function
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 15:13:47 +0100 |
chaieb |
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
|
file |
diff |
annotate
|
| Sat, 06 Jan 2007 20:47:09 +0100 |
chaieb |
A few theorems on integer divisibily.
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:16 +0100 |
haftmann |
clarified module dependencies
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Thu, 09 Feb 2006 12:14:39 +0100 |
paulson |
names for simprules
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 15:12:59 +0100 |
nipkow |
made "dvd" on numbers executable by simp.
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 10:59:55 +0100 |
paulson |
tidied, and giving theorems names
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 15:36:28 +0200 |
paulson |
classical rules must have names for ATP integration
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
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
|
| Wed, 23 Mar 2005 12:09:18 +0100 |
paulson |
replaced bool by a new datatype "bit" for binary numerals
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 10:23:36 +0100 |
berghofe |
New theorem zpower_int
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Fri, 01 Oct 2004 11:53:31 +0200 |
paulson |
tweaking of arithmetic proofs
|
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
|
| Mon, 02 Aug 2004 16:06:13 +0200 |
obua |
zdiv_int, zmod_int
|
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
|
| 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
|
| 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
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
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, 28 Jan 2003 07:39:29 +0100 |
nipkow |
pos/neg_mod_sign/bound are now simp rules.
|
file |
diff |
annotate
|
| Fri, 15 Nov 2002 18:02:25 +0100 |
nipkow |
added zdvd_iff_zmod_eq_0
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:03:05 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Mon, 01 Jul 2002 17:42:08 +0200 |
nipkow |
modified Larry's changes to make div/mod a numeral work in arith.
|
file |
diff |
annotate
|
| Sat, 29 Jun 2002 22:46:56 +0200 |
paulson |
new splitting rules for zdiv, zmod
|
file |
diff |
annotate
|
| Tue, 28 May 2002 11:06:06 +0200 |
paulson |
conversion of IntDiv.thy to Isar format
|
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
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Sun, 21 May 2000 14:49:28 +0200 |
wenzelm |
replaced {{ }} by { };
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:47:16 +0200 |
wenzelm |
IntArith;
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:45:47 +0200 |
paulson |
change to force (m div 0 = 0)
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|