| 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
|