src/HOL/Integ/reflected_presburger.ML
2005-09-15 chaieb 2005-09-15 getting it work for SMLNJ
2005-09-15 haftmann 2005-09-15 fixed type annotation
2005-09-14 chaieb 2005-09-14 Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
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