equal
deleted
inserted
replaced
56 qed |
56 qed |
57 |
57 |
58 end |
58 end |
59 |
59 |
60 text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence |
60 text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence |
61 classes} over elements of the base type @{typ 'a}.\<close> |
61 classes} over elements of the base type \<^typ>\<open>'a\<close>.\<close> |
62 |
62 |
63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
64 |
64 |
65 typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" |
65 typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" |
66 unfolding quot_def by blast |
66 unfolding quot_def by blast |