src/HOL/ex/Commutative_Ring_Complete.thy
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-05 wenzelm 2007-06-05 tuned document;
2007-04-20 haftmann 2007-04-20 switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-09-14 wenzelm 2005-09-14 imports Commutative_Ring instead of Main, since the latter hides our names;
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
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