src/HOL/Int.thy
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-12-10 paulson 2009-12-10 streamlined proofs
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-11-08 wenzelm 2009-11-08 modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-29 haftmann 2009-10-29 moved some dvd [int] facts to Int
2009-10-29 haftmann 2009-10-29 moved some dvd [int] facts to Int
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-10-21 blanchet 2009-10-21 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-08-28 nipkow 2009-08-28 tuned proofs
2009-07-29 haftmann 2009-07-29 added numeral code postprocessor rules on type int
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-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-08 haftmann 2009-05-08 moved int_factor_simprocs.ML to theory Int
2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-28 haftmann 2009-04-28 reorganization of power lemmas
2009-04-28 haftmann 2009-04-28 local syntax for Ints; ephermal re-globalization
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