src/HOL/Library/Quotient.thy
changeset 12338 de0f4a63baa5
parent 11549 e7265e70fd7c
child 12371 80ca9058db95
     1.1 --- a/src/HOL/Library/Quotient.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4   "\<sim> :: 'a => 'a => bool"}.
     1.5  *}
     1.6  
     1.7 -axclass eqv \<subseteq> "term"
     1.8 +axclass eqv \<subseteq> type
     1.9  consts
    1.10    eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
    1.11