src/HOL/Int.thy
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-04-01 nipkow 2009-04-01 cleaned up setprod_zero-related lemmas
2009-04-01 nipkow 2009-04-01 added setsum_pos_nat
2009-03-30 huffman 2009-03-30 simplify theorem references
2009-03-30 huffman 2009-03-30 no longer delay loading of assoc_fold.ML
2009-03-22 haftmann 2009-03-22 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
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-03-02 nipkow 2009-03-02 name changes
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-19 huffman 2009-02-19 declare of_int_number_of_eq [simp]
2009-02-16 blanchet 2009-02-16 Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.
2009-02-03 krauss 2009-02-03 declare "nat o abs" as default measure for int
2009-01-31 nipkow 2009-01-31 added some simp rules
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-26 haftmann 2009-01-26 stripped Id
2009-01-21 haftmann 2009-01-21 no base sort in class import
2008-12-10 huffman 2008-12-10 clean up diff_bin_simps
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-04 huffman 2008-12-04 revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
2008-12-04 huffman 2008-12-04 add named lemma lists: neg_simps and iszero_simps
2008-12-04 huffman 2008-12-04 change arith_special simps to avoid using neg
2008-12-03 huffman 2008-12-03 enable eq_bin_simps for simplifying equalities on numerals
2008-12-03 huffman 2008-12-03 enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
2008-12-03 huffman 2008-12-03 cleaned up subsection headings; added simp rules for comparisons on binary numbers
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-11-10 haftmann 2008-11-10 tuned
2008-10-22 haftmann 2008-10-22 slightly tuned
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-10-07 haftmann 2008-10-07 tuned of_nat code generation
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-07-25 haftmann 2008-07-25 added class preorder
2008-06-30 haftmann 2008-06-30 code generator setup for "int" also works under eta-contraction
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-02 haftmann 2008-04-02 moved some code lemmas for Numerals here
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-16 huffman 2008-02-16 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-21 haftmann 2008-01-21 tuned code setup
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int