src/HOL/Algebra/QuotRing.thy
Thu, 21 Jun 2007 17:28:53 +0200 wenzelm tuned proofs -- avoid implicit prems;
less more (0) -1 tip