src/HOL/Presburger.thy
22 months ago blanchet 2017-09-08 speed up proofs slightly
2016-10-16 haftmann 2016-10-16 avoid effectively subsumed rules; simplified fact reference
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 clarified theorem names
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-09-29 boehmes 2016-09-29 use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
2016-09-29 boehmes 2016-09-29 invoke argo as part of the tried automatic proof methods
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-07 wenzelm 2014-11-07 more accurate keywords;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-10-23 haftmann 2014-10-23 further downshift of theory Parity in the hierarchy
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-04 blanchet 2014-05-04 added 'satx' proof method to Try0
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