# HG changeset patch
# User wenzelm
# Date 972331903 -7200
# Node ID 3b53ed2c846f00c5603cfc516d8508429ea9daab
# Parent  d78de58fe3689144e73d2d863b88f470addbae5f
tuned;

diff -r d78de58fe368 -r 3b53ed2c846f src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Mon Oct 23 22:11:24 2000 +0200
+++ b/src/HOL/Calculation.thy	Mon Oct 23 22:11:43 2000 +0200
@@ -153,7 +153,7 @@
   Note that this list of rules is in reverse order of priorities.
 *}
 
-lemmas trans_rules [trans] =
+lemmas basic_trans_rules [trans] =
   order_less_subst2
   order_less_subst1
   order_le_less_subst2
diff -r d78de58fe368 -r 3b53ed2c846f src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:24 2000 +0200
+++ b/src/HOL/Library/Quotient.thy	Mon Oct 23 22:11:43 2000 +0200
@@ -54,7 +54,7 @@
   equivalence_class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
 
-theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
+theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
   fix R assume R: "A = Abs_quot R"
   assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
@@ -62,9 +62,8 @@
   thus ?thesis by (unfold equivalence_class_def)
 qed
 
-lemma quot_cases [case_names rep, cases type: quot]:
-    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
-  by (insert quot_rep) blast
+lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
+  by (insert quot_exhaust) blast
 
 
 subsection {* Equality on quotients *}