src/HOL/Int.thy
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-02-19 kuncar 2013-02-19 delete also predicates on relations when hiding an implementation of an abstract type
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-06-02 huffman 2012-06-02 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
2012-05-30 huffman 2012-05-30 convert Int.thy to use lifting and transfer
2012-05-30 huffman 2012-05-30 remove unnecessary simp rules involving Abs_Integ
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-30 huffman 2012-03-30 load Tools/numeral.ML in Num.thy
2012-03-30 huffman 2012-03-30 set up numeral reorient simproc in Num.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 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)
2012-03-02 bulwahn 2012-03-02 adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
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; attribute code_abbrev superseedes code_unfold_post
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-17 huffman 2011-11-17 simplify some proofs
2011-11-17 huffman 2011-11-17 Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
2011-10-20 huffman 2011-10-20 removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
2011-10-19 wenzelm 2011-10-19 inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for integers
2011-10-09 huffman 2011-10-09 Int.thy: discontinued some legacy theorems
2011-09-04 huffman 2011-09-04 introduce abbreviation 'int' earlier in Int.thy
2011-09-04 huffman 2011-09-04 move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-03 huffman 2011-09-03 remove duplicate lemma nat_zero in favor of nat_0
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-06-23 huffman 2011-06-23 added number_semiring class, plus a few new lemmas; no changes to the simpset yet
2011-05-04 wenzelm 2011-05-04 proper case_names for int_cases, int_of_nat_induct; tuned some proofs, eliminating (cases, auto) anti-pattern;
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-11-30 haftmann 2010-11-30 adapted proofs to slightly changed definitions of congruent(2)
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-11 haftmann 2010-05-11 renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-10 haftmann 2010-05-10 moved int induction lemma to theory Int as int_bidirectional_induct
2010-05-07 haftmann 2010-05-07 moved lemma zdvd_period to theory Int
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-04-27 haftmann 2010-04-27 got rid of [simplified]
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-06 boehmes 2010-04-06 added missing mult_1_left to linarith simp rules
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 boehmes 2010-03-17 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-07 huffman 2010-03-07 add more simp rules for Ints
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
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;