| Fri, 30 Mar 2012 12:32:35 +0200 |
huffman |
replace lemmas eval_nat_numeral with a simpler reformulation
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 11:52:26 +0200 |
huffman |
new lemmas for simplifying subtraction on nat numerals
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 11:16:35 +0200 |
huffman |
removed redundant nat-specific copies of theorems
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 10:41:27 +0200 |
huffman |
move more theorems from Nat_Numeral.thy to Num.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:04:28 +0200 |
huffman |
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 09:08:29 +0200 |
huffman |
add constant pred_numeral k = numeral k - (1::nat);
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:11:52 +0200 |
huffman |
move lemmas from Nat_Numeral.thy to Nat.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:10:28 +0200 |
huffman |
move lemmas from Nat_Numeral to Int.thy and Num.thy
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 14:47:31 +0200 |
huffman |
remove obsolete simp rule for powers
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 14:42:55 +0200 |
huffman |
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 14:39:05 +0200 |
huffman |
remove unneeded rewrite rules for powers of numerals
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 14:29:36 +0200 |
huffman |
remove duplicate lemma Suc_numeral
|
file |
diff |
annotate
|
| 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
|
| Thu, 06 May 2010 23:11:56 +0200 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| Thu, 06 May 2010 18:16:07 +0200 |
haftmann |
moved generic lemmas to appropriate places
|
file |
diff |
annotate
|
| Wed, 05 May 2010 16:53:21 +0200 |
haftmann |
moved nat_arith ot Nat_Numeral: clarified normalizer setup
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 18:24:30 -0800 |
huffman |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:27 +0100 |
haftmann |
hide fact Nat.add_0_right; make add_0_right from Groups priority
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:22:22 +0100 |
haftmann |
dropped accidental duplication of "lin" prefix from cs. 108662d50512
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 22:16:12 +0100 |
haftmann |
moved some lemmas to theory Int
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:18 +0200 |
haftmann |
tuned code postprocessor
|
file |
diff |
annotate
|
| Mon, 11 May 2009 19:51:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Mon, 11 May 2009 08:28:49 -0700 |
huffman |
newline at end of file
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Mon, 04 May 2009 14:49:49 +0200 |
haftmann |
dropped duplicate lemma sum_nonneg_eq_zero_iff
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:29 +0200 |
haftmann |
collected square lemmas in Nat_Numeral
|
file |
diff |
annotate
|
| Mon, 27 Apr 2009 10:11:46 +0200 |
haftmann |
whitespace tuning
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:30:39 +0200 |
haftmann |
theory NatBin now named Nat_Numeral
|
file |
diff |
annotate
| base
|