src/HOL/Library/Quotient.thy
changeset 10311 3b53ed2c846f
parent 10286 fdcdb8a80988
child 10333 f12ff6a4bc7b
     1.1 --- a/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:24 2000 +0200
     1.2 +++ b/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:43 2000 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    equivalence_class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     1.5    "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
     1.6  
     1.7 -theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
     1.8 +theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
     1.9  proof (cases A)
    1.10    fix R assume R: "A = Abs_quot R"
    1.11    assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
    1.12 @@ -62,9 +62,8 @@
    1.13    thus ?thesis by (unfold equivalence_class_def)
    1.14  qed
    1.15  
    1.16 -lemma quot_cases [case_names rep, cases type: quot]:
    1.17 -    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    1.18 -  by (insert quot_rep) blast
    1.19 +lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    1.20 +  by (insert quot_exhaust) blast
    1.21  
    1.22  
    1.23  subsection {* Equality on quotients *}