| Mon, 23 Mar 2009 19:01:15 +0100 |
haftmann |
structure LinArith now named Lin_Arith
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:10 +0100 |
haftmann |
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
strippd Id
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 24 Feb 2009 11:10:05 -0800 |
huffman |
add simp rules for numerals with 1::nat
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 16:25:52 -0800 |
huffman |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 10:03:58 +0000 |
paulson |
Even and odd powers of -1
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 11:49:23 -0800 |
huffman |
rename abbreviation square -> power2, to match theorem names
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 07:52:54 -0800 |
huffman |
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 20:36:20 -0800 |
huffman |
separate neg_simps from rel_simps
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 19:39:53 -0800 |
huffman |
change lemmas to avoid using neg
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 17:35:22 -0800 |
huffman |
simplify less_nat_number_of
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 17:26:16 -0800 |
huffman |
add lemma le_nat_number_of
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 11:14:24 -0800 |
huffman |
change arith_special simps to avoid using neg
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 08:47:45 -0800 |
huffman |
change more lemmas to avoid using iszero
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 22:16:20 -0800 |
huffman |
change some lemmas to avoid using iszero
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 20:24:17 -0800 |
huffman |
simplify proof of less_nat_number_of
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:26 +0200 |
haftmann |
dropped superfluous code lemmas
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:34 +0100 |
haftmann |
dropped legacy ml bindings
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:24 +0200 |
wenzelm |
tuned LinArith setup;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 19:58:53 +0200 |
nipkow |
Added cancel simprocs for dvd on nat and int
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 05:20:05 +0200 |
huffman |
modify proofs to avoid referring to int::nat=>int
|
file |
diff |
annotate
|
| Fri, 08 Jun 2007 03:24:27 +0200 |
huffman |
generalize zpower_number_of_{even,odd} lemmas
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 17:01:33 +0200 |
huffman |
generalize class constraints on some lemmas
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|