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