tuned;
authorwenzelm
Mon Oct 23 22:11:43 2000 +0200 (2000-10-23)
changeset 103113b53ed2c846f
parent 10310 d78de58fe368
child 10312 4c5a03649af7
tuned;
src/HOL/Calculation.thy
src/HOL/Library/Quotient.thy
     1.1 --- a/src/HOL/Calculation.thy	Mon Oct 23 22:11:24 2000 +0200
     1.2 +++ b/src/HOL/Calculation.thy	Mon Oct 23 22:11:43 2000 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4    Note that this list of rules is in reverse order of priorities.
     1.5  *}
     1.6  
     1.7 -lemmas trans_rules [trans] =
     1.8 +lemmas basic_trans_rules [trans] =
     1.9    order_less_subst2
    1.10    order_less_subst1
    1.11    order_le_less_subst2
     2.1 --- a/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:24 2000 +0200
     2.2 +++ b/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:43 2000 +0200
     2.3 @@ -54,7 +54,7 @@
     2.4    equivalence_class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     2.5    "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
     2.6  
     2.7 -theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
     2.8 +theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
     2.9  proof (cases A)
    2.10    fix R assume R: "A = Abs_quot R"
    2.11    assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
    2.12 @@ -62,9 +62,8 @@
    2.13    thus ?thesis by (unfold equivalence_class_def)
    2.14  qed
    2.15  
    2.16 -lemma quot_cases [case_names rep, cases type: quot]:
    2.17 -    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    2.18 -  by (insert quot_rep) blast
    2.19 +lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    2.20 +  by (insert quot_exhaust) blast
    2.21  
    2.22  
    2.23  subsection {* Equality on quotients *}