src/HOL/ex/PresburgerEx.thy
2009-02-02 haftmann 2009-02-02 updated class documentation
2008-01-03 chaieb 2008-01-03 Tuned (type information in Lemmas)
2007-08-22 chaieb 2007-08-22 imports Presburger; no need for Main
2007-06-21 wenzelm 2007-06-21 renamed NatSimprocs.thy to Arith_Tools.thy; incorporated HOL/Presburger.thy into NatSimprocs.thy;
2007-06-11 chaieb 2007-06-11 Added more examples
2006-09-21 wenzelm 2006-09-21 updated timings;
2006-06-08 nipkow 2006-06-08 added John's example
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-07-22 webertj 2004-07-22 minor formatting fixes
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-19 chaieb 2004-05-19 A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2003-03-25 berghofe 2003-03-25 Added examples for Presburger arithmetic.