# HG changeset patch
# User wenzelm
# Date 973283759 -3600
# Node ID 1d54567bed24eaa6863dc7d628b7d310c7476274
# Parent  c7d8901ab269aaa2527fb70d896fe74cce697229
tuned;

diff -r c7d8901ab269 -r 1d54567bed24 src/HOL/Library/Quotient.thy
--- 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"