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