| Thu, 29 Mar 2012 14:09:10 +0200 |
huffman |
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sun, 11 Sep 2011 09:40:18 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 09:31:04 -0700 |
huffman |
generalize lemma of_nat_number_of_eq to class number_semiring
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 09:59:28 -0700 |
huffman |
add lemma power2_eq_iff
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 09:04:20 -0700 |
huffman |
added number_semiring class, plus a few new lemmas;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 15:58:55 -0700 |
huffman |
generalize lemmas power_number_of_even and power_number_of_odd
|
file |
diff |
annotate
|
| Thu, 25 Nov 2010 00:17:16 +0100 |
blanchet |
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
|
file |
diff |
annotate
|
| Sun, 24 Oct 2010 20:19:00 +0200 |
nipkow |
nat_number -> eval_nat_numeral
|
file |
diff |
annotate
|
| Mon, 17 May 2010 08:40:17 -0700 |
huffman |
remove simp attribute from power2_eq_1_iff
|
file |
diff |
annotate
|
| Tue, 11 May 2010 19:01:35 -0700 |
huffman |
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
|
file |
diff |
annotate
|
| Tue, 11 May 2010 06:27:06 -0700 |
huffman |
add lemma power2_eq_1_iff; generalize some other lemmas
|
file |
diff |
annotate
|