src/HOL/Library/Quotient_Type.thy
changeset 49834 b27bbb021df1
parent 45694 4a8743618257
child 58881 b9556a055632
--- a/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -60,7 +60,7 @@
 
 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
 
-typedef (open) 'a quot = "quot :: 'a::eqv set set"
+typedef 'a quot = "quot :: 'a::eqv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"