src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
2011-09-07 wenzelm 2011-09-07 tuned proofs;
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs