src/HOL/Library/Quotient.thy
changeset 10390 1d54567bed24
parent 10333 f12ff6a4bc7b
child 10392 f27afee8475d
     1.1 --- a/src/HOL/Library/Quotient.thy	Fri Nov 03 21:35:36 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Fri Nov 03 21:35:59 2000 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4  subsection {* Equivalence relations and quotient types *}
     1.5  
     1.6  text {*
     1.7 - \medskip Type class @{text equiv} models equivalence relations using
     1.8 - the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation.
     1.9 + \medskip Type class @{text equiv} models equivalence relations @{text
    1.10 + "\<sim> :: 'a => 'a => bool"}.
    1.11  *}
    1.12  
    1.13  axclass eqv < "term"