tuned;

--- a/src/HOL/Library/Quotient.thy	Fri Nov 03 21:35:36 2000 +0100
+++ b/src/HOL/Library/Quotient.thy	Fri Nov 03 21:35:59 2000 +0100
@@ -18,8 +18,8 @@
 subsection {* Equivalence relations and quotient types *}
 
 text {*
- \medskip Type class @{text equiv} models equivalence relations using
- the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation.
+ \medskip Type class @{text equiv} models equivalence relations @{text
+ "\<sim> :: 'a => 'a => bool"}.
 *}
 
 axclass eqv < "term"