summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Quotient.thy

changeset 18730 | 843da46f89ac |

parent 18551 | be0705186ff5 |

child 19086 | 1b3780be6cc2 |

--- a/src/HOL/Library/Quotient.thy Sat Jan 21 23:02:20 2006 +0100 +++ b/src/HOL/Library/Quotient.thy Sat Jan 21 23:02:21 2006 +0100 @@ -64,10 +64,10 @@ by blast lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" - by (unfold quot_def) blast + unfolding quot_def by blast lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" - by (unfold quot_def) blast + unfolding quot_def by blast text {* \medskip Abstracted equivalence classes are the canonical @@ -83,11 +83,11 @@ fix R assume R: "A = Abs_quot R" assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast - thus ?thesis by (unfold class_def) + thus ?thesis unfolding class_def . qed lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" - by (insert quot_exhaust) blast + using quot_exhaust by blast subsection {* Equality on quotients *}