equal
deleted
inserted
replaced
152 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
152 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
153 \<close> |
153 \<close> |
154 |
154 |
155 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}" |
155 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}" |
156 |
156 |
157 typedef 'a quot = "quot :: 'a::partial_equiv set set" |
157 typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set" |
158 unfolding quot_def by blast |
158 unfolding quot_def by blast |
159 |
159 |
160 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
160 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
161 unfolding quot_def by blast |
161 unfolding quot_def by blast |
162 |
162 |