src/HOL/Presburger.thy
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
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.