src/HOL/NatBin.thy
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-24 huffman 2009-02-24 add simp rules for numerals with 1::nat
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-17 paulson 2009-02-17 Even and odd powers of -1
2009-01-06 huffman 2009-01-06 rename abbreviation square -> power2, to match theorem names
2008-12-10 huffman 2008-12-10 move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
2008-12-09 huffman 2008-12-09 move all neg-related lemmas to NatBin; make type of neg specific to int
2008-12-09 huffman 2008-12-09 separate neg_simps from rel_simps
2008-12-06 huffman 2008-12-06 change lemmas to avoid using neg
2008-12-05 huffman 2008-12-05 simplify less_nat_number_of
2008-12-05 huffman 2008-12-05 add lemma le_nat_number_of
2008-12-04 huffman 2008-12-04 change arith_special simps to avoid using neg
2008-12-04 huffman 2008-12-04 change more lemmas to avoid using iszero
2008-12-03 huffman 2008-12-03 change some lemmas to avoid using iszero
2008-12-03 huffman 2008-12-03 simplify proof of less_nat_number_of
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-16 haftmann 2008-09-16 dropped superfluous code lemmas
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-24 nipkow 2007-07-24 Added cancel simprocs for dvd on nat and int
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 huffman 2007-06-11 modify proofs to avoid referring to int::nat=>int
2007-06-08 huffman 2007-06-08 generalize zpower_number_of_{even,odd} lemmas
2007-06-06 huffman 2007-06-06 generalize class constraints on some lemmas
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;