src/HOL/Tools/Qelim/presburger.ML
2009-03-03 nipkow 2009-03-03 removed and renamed redundant lemmas
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-17 chaieb 2009-02-17 merged
2009-02-17 chaieb 2009-02-17 fixed selection of premises
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-05-29 wenzelm 2008-05-29 proper context for ss;
2008-01-05 chaieb 2008-01-05 Tuned relevant premises selection
2008-01-03 chaieb 2008-01-03 tuned relevance test for presburger
2008-01-03 chaieb 2008-01-03 Changed order of tactics in presburger --- thinning before case splits
2008-01-02 haftmann 2008-01-02 some more antiquotations
2007-10-12 haftmann 2007-10-12 moved class power to theory Power
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-22 chaieb 2007-08-22 More selective generalization : a*b is generalized whenever none of a and b is a number
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical;
2007-06-25 wenzelm 2007-06-25 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW; eta_long_tac; tuned;
2007-06-25 wenzelm 2007-06-25 Thm.eta_long_conversion;
2007-06-21 huffman 2007-06-21 add thm antiquotations
2007-06-21 wenzelm 2007-06-21 moved quantifier elimination tools to Tools/Qelim/;