src/HOL/Library/Quotient.thy

 text {*
  \medskip Type class @{text equiv} models equivalence relations @{text
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-class eqv = type +
+class eqv =
   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
 
 class equiv = eqv +
   assumes equiv_refl [intro]: "x \<sim> x"
   assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"