src/HOL/Library/Quotient_Type.thy
changeset 61260 e6f03fae14d5
parent 59192 a1d6d6db781b
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/Quotient_Type.thy	Wed Sep 23 09:50:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Type.thy	Thu Sep 24 13:33:42 2015 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
     1.6  
     1.7 -typedef 'a quot = "quot :: 'a::eqv set set"
     1.8 +typedef (overloaded) 'a quot = "quot :: 'a::eqv set set"
     1.9    unfolding quot_def by blast
    1.10  
    1.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"