src/HOL/Presburger.thy
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;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-12 chaieb 2007-06-12 Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
2007-06-11 chaieb 2007-06-11 A new and cleaned up Theory for QE. for Presburger arithmetic
2007-06-05 wenzelm 2007-06-05 tuned comments;
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2007-05-31 wenzelm 2007-05-31 fixed title;
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2007-04-26 haftmann 2007-04-26 cleaned up code generator setup for int
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-03-02 haftmann 2007-03-02 tuned code theorems for ord on integers
2007-01-06 chaieb 2007-01-06 A few theorems on integer divisibily.
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-09-19 haftmann 2006-09-19 improved numeral handling for nbe
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-08 wenzelm 2006-07-08 tuned;
2005-11-18 chaieb 2005-11-18 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-14 chaieb 2005-09-14 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring
2005-07-14 wenzelm 2005-07-14 improved oracle setup;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-08-18 nipkow 2004-08-18 import -> imports