src/HOL/Library/Quotient.thy
changeset 29608 564ea783ace8
parent 27487 c8a6ce181805
child 30738 0842e906300c
--- a/src/HOL/Library/Quotient.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Library/Quotient.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -21,7 +21,7 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-class eqv = type +
+class eqv =
   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
 
 class equiv = eqv +