equal
deleted
inserted
replaced
58 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
58 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
59 *} |
59 *} |
60 |
60 |
61 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}" |
61 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}" |
62 |
62 |
63 typedef (open) 'a quot = "quot :: 'a::eqv set set" |
63 typedef 'a quot = "quot :: 'a::eqv set set" |
64 unfolding quot_def by blast |
64 unfolding quot_def by blast |
65 |
65 |
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
67 unfolding quot_def by blast |
67 unfolding quot_def by blast |
68 |
68 |