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