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