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 +