src/HOL/ex/Reflected_Presburger.thy
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-09-23 webertj 2005-09-23 some typos in comments fixed
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-09-14 chaieb 2005-09-14 tactic and the rest eliminated, just the theory....
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