src/HOL/Presburger.thy
2013-10-31 haftmann 2013-10-31 moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger
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-04-12 wenzelm 2012-04-12 more standard method setup;
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-09 wenzelm 2011-11-09 avoid inconsistent sort constraints;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2010-05-10 haftmann 2010-05-10 shorten names
2010-05-10 haftmann 2010-05-10 updated references to ML files
2010-05-10 haftmann 2010-05-10 only one module fpr presburger method
2010-05-10 haftmann 2010-05-10 tuned theory text; dropped unused lemma
2010-05-10 haftmann 2010-05-10 one structure is better than three
2010-05-10 haftmann 2010-05-10 less complex organization of cooper source code
2010-05-07 haftmann 2010-05-07 moved lemma zdvd_period to theory Int
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-09-10 haftmann 2009-09-10 cleanedup theorems all_nat ex_nat
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-22 haftmann 2009-03-22 moved import of module qelim to theory Presburger
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-20 nipkow 2009-02-20 removed subsumed lemmas
2009-02-02 haftmann 2009-02-02 dropped Id
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-03 huffman 2008-12-03 enable eq_bin_simps for simplifying equalities on numerals
2008-09-29 haftmann 2008-09-29 clarified dependencies between arith tools
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-07-21 chaieb 2008-07-21 Tuned and simplified proofs
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-11 haftmann 2008-07-11 separate class dvd for divisibility predicate
2008-04-02 haftmann 2008-04-02 moved some code lemmas for Numerals to other theories
2008-02-27 chaieb 2008-02-27 loads Tools/Qelim/qelim.ML
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-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-08-22 chaieb 2007-08-22 tuned;
2007-07-31 wenzelm 2007-07-31 proper context for cooper_tac within arith;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-19 haftmann 2007-07-19 code lemma for of_int
2007-07-10 haftmann 2007-07-10 moved lemma zdvd_period here
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-21 huffman 2007-06-21 section headings
2007-06-21 wenzelm 2007-06-21 moved Presburger setup back to Presburger.thy;
2007-06-21 wenzelm 2007-06-21 adapted tool setup;
2007-06-20 huffman 2007-06-20 remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20 huffman 2007-06-20 section headings
2007-06-17 chaieb 2007-06-17 moved lemma all_not_ex to HOL.thy ; tuned proofs
2007-06-14 chaieb 2007-06-14 Added some lemmas to default presburger simpset; tuned proofs
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;