src/HOL/Library/Quotient_Type.thy
changeset 45694 4a8743618257
parent 35100 53754ec7360b
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -58,8 +58,10 @@
     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 -  by blast
     1.9 +definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
    1.10 +
    1.11 +typedef (open) 'a quot = "quot :: 'a::eqv set set"
    1.12 +  unfolding quot_def by blast
    1.13  
    1.14  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    1.15    unfolding quot_def by blast