src/HOL/Integ/Presburger.thy
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-14 chaieb 2004-06-14 Oracle corrected
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-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
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-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-08-05 nipkow 2003-08-05 cleaned up
2003-03-25 berghofe 2003-03-25 New decision procedure for Presburger arithmetic.