src/HOL/Nat_Numeral.thy
2012-03-30 huffman 2012-03-30 replace lemmas eval_nat_numeral with a simpler reformulation
2012-03-30 huffman 2012-03-30 new lemmas for simplifying subtraction on nat numerals
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-30 huffman 2012-03-30 move more theorems from Nat_Numeral.thy to Num.thy
2012-03-30 huffman 2012-03-30 move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
2012-03-30 huffman 2012-03-30 add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
2012-03-30 huffman 2012-03-30 move lemmas from Nat_Numeral.thy to Nat.thy
2012-03-30 huffman 2012-03-30 move lemmas from Nat_Numeral to Int.thy and Num.thy
2012-03-29 huffman 2012-03-29 remove obsolete simp rule for powers
2012-03-29 huffman 2012-03-29 remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
2012-03-29 huffman 2012-03-29 remove unneeded rewrite rules for powers of numerals
2012-03-29 huffman 2012-03-29 remove duplicate lemma Suc_numeral
2012-03-29 huffman 2012-03-29 move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-11 huffman 2011-09-11 tuned proofs
2011-09-09 huffman 2011-09-09 generalize lemma of_nat_number_of_eq to class number_semiring
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-08-20 huffman 2011-08-20 add lemma power2_eq_iff
2011-06-23 huffman 2011-06-23 added number_semiring class, plus a few new lemmas; no changes to the simpset yet
2011-06-22 huffman 2011-06-22 generalize lemmas power_number_of_even and power_number_of_odd
2010-11-25 blanchet 2010-11-25 added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2010-05-17 huffman 2010-05-17 remove simp attribute from power2_eq_1_iff
2010-05-11 huffman 2010-05-11 include iszero_simps in semiring_norm just once (they are already included in rel_simps)
2010-05-11 huffman 2010-05-11 add lemma power2_eq_1_iff; generalize some other lemmas
2010-05-06 haftmann 2010-05-06 moved some lemmas from Groebner_Basis here
2010-05-06 haftmann 2010-05-06 moved generic lemmas to appropriate places
2010-05-05 haftmann 2010-05-05 moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-03-17 boehmes 2010-03-17 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-06 huffman 2010-03-06 generalize some lemmas from class linordered_ring_strict to linordered_ring
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-08 haftmann 2010-02-08 hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-29 haftmann 2009-10-29 moved some lemmas to theory Int
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-05-15 haftmann 2009-05-15 tuned code postprocessor
2009-05-11 haftmann 2009-05-11 merged
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-11 huffman 2009-05-11 newline at end of file
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-04 haftmann 2009-05-04 dropped duplicate lemma sum_nonneg_eq_zero_iff
2009-04-28 haftmann 2009-04-28 collected square lemmas in Nat_Numeral
2009-04-27 haftmann 2009-04-27 whitespace tuning
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-04-15 haftmann 2009-04-15 theory NatBin now named Nat_Numeral