--- a/QuotScript.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -53,7 +53,7 @@
 using a unfolding Quotient_def
 by blast
 
-lemma Quotient_REL:
+lemma Quotient_rel:
   assumes a: "Quotient E Abs Rep"
   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
 using a unfolding Quotient_def
@@ -251,7 +251,7 @@
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))
-apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1])
+apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1])
 done
 
 (* ask Peter: fun_rel_IMP used twice *) 
@@ -328,14 +328,14 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
 (* Not used *)
 lemma REP_ABS_RSP_LEFT:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)