src/HOL/Library/Quotient.thy
changeset 22473 753123c89d72
parent 22390 378f34b1e380
child 23373 ead82c82da9e
     1.1 --- a/src/HOL/Library/Quotient.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4   "\<sim> :: 'a => 'a => bool"}.
     1.5  *}
     1.6  
     1.7 -class eqv =
     1.8 +class eqv = type +
     1.9    fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
    1.10  
    1.11  class equiv = eqv +