src/HOL/Library/Quotient.thy
 changeset 10551 ec9fab41b3a0 parent 10505 b89e6cc963e3 child 10681 ec76e17f73c5
```     1.1 --- a/src/HOL/Library/Quotient.thy	Thu Nov 30 20:05:10 2000 +0100
1.2 +++ b/src/HOL/Library/Quotient.thy	Thu Nov 30 20:05:34 2000 +0100
1.3 @@ -76,7 +76,7 @@
1.4  *}
1.5
1.6  constdefs
1.7 -  equivalence_class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
1.8 +  class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
1.9    "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
1.10
1.11  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
1.12 @@ -84,7 +84,7 @@
1.13    fix R assume R: "A = Abs_quot R"
1.14    assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
1.15    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
1.16 -  thus ?thesis by (unfold equivalence_class_def)
1.17 +  thus ?thesis by (unfold class_def)
1.18  qed
1.19
1.20  lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
1.21 @@ -104,7 +104,7 @@
1.22    show "a \<sim> b"
1.23    proof -
1.24      from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
1.25 -      by (simp only: equivalence_class_def Abs_quot_inject quotI)
1.26 +      by (simp only: class_def Abs_quot_inject quotI)
1.27      moreover have "a \<sim> a" ..
1.28      ultimately have "a \<in> {x. b \<sim> x}" by blast
1.29      hence "b \<sim> a" by blast
1.30 @@ -127,7 +127,7 @@
1.31          finally show "a \<sim> x" .
1.32        qed
1.33      qed
1.34 -    thus ?thesis by (simp only: equivalence_class_def)
1.35 +    thus ?thesis by (simp only: class_def)
1.36    qed
1.37  qed
1.38
```