src/HOL/Library/Quotient.thy
changeset 18730 843da46f89ac
parent 18551 be0705186ff5
child 19086 1b3780be6cc2
     1.1 --- a/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:20 2006 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:21 2006 +0100
     1.3 @@ -64,10 +64,10 @@
     1.4    by blast
     1.5  
     1.6  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
     1.7 -  by (unfold quot_def) blast
     1.8 +  unfolding quot_def by blast
     1.9  
    1.10  lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    1.11 -  by (unfold quot_def) blast
    1.12 +  unfolding quot_def by blast
    1.13  
    1.14  text {*
    1.15   \medskip Abstracted equivalence classes are the canonical
    1.16 @@ -83,11 +83,11 @@
    1.17    fix R assume R: "A = Abs_quot R"
    1.18    assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
    1.19    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    1.20 -  thus ?thesis by (unfold class_def)
    1.21 +  thus ?thesis unfolding class_def .
    1.22  qed
    1.23  
    1.24  lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    1.25 -  by (insert quot_exhaust) blast
    1.26 +  using quot_exhaust by blast
    1.27  
    1.28  
    1.29  subsection {* Equality on quotients *}