src/HOL/Library/Quotient.thy
changeset 10392 f27afee8475d
parent 10390 1d54567bed24
child 10437 7528f9e30ca4
     1.1 --- a/src/HOL/Library/Quotient.thy	Sat Nov 04 18:39:44 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Sat Nov 04 18:41:37 2000 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4   \emph{equivalence classes} over elements of the base type @{typ 'a}.
     1.5  *}
     1.6  
     1.7 -typedef 'a quot = "{{x. a \<sim> x}| a::'a::eqv. True}"
     1.8 +typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
     1.9    by blast
    1.10  
    1.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"