summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 30 Nov 2000 20:05:34 +0100 | |

changeset 10551 | ec9fab41b3a0 |

parent 10550 | 93ca45370c59 |

child 10552 | a177b8571026 |

renamed "equivalence_class" to "class";

--- a/src/HOL/Library/Quotient.thy Thu Nov 30 20:05:10 2000 +0100 +++ b/src/HOL/Library/Quotient.thy Thu Nov 30 20:05:34 2000 +0100 @@ -76,7 +76,7 @@ *} constdefs - equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") + class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" @@ -84,7 +84,7 @@ 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 equivalence_class_def) + thus ?thesis by (unfold class_def) qed lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" @@ -104,7 +104,7 @@ show "a \<sim> b" proof - from eq have "{x. a \<sim> x} = {x. b \<sim> x}" - by (simp only: equivalence_class_def Abs_quot_inject quotI) + by (simp only: class_def Abs_quot_inject quotI) moreover have "a \<sim> a" .. ultimately have "a \<in> {x. b \<sim> x}" by blast hence "b \<sim> a" by blast @@ -127,7 +127,7 @@ finally show "a \<sim> x" . qed qed - thus ?thesis by (simp only: equivalence_class_def) + thus ?thesis by (simp only: class_def) qed qed