--- a/QuotScript.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -41,7 +41,7 @@
                         (\<forall>a. E (Rep a) (Rep a)) \<and> 
                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
-lemma Quotient_ABS_REP:
+lemma Quotient_abs_rep:
   assumes a: "Quotient E Abs Rep"
   shows "Abs (Rep a) = a" 
 using a unfolding Quotient_def
@@ -77,7 +77,7 @@
 using a unfolding Quotient_def
 by metis
 
-lemma Quotient_REP_ABS:
+lemma Quotient_rep_abs:
   assumes a: "Quotient R Abs Rep"
   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
 using a unfolding Quotient_def
@@ -283,7 +283,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 lemma lambda_prs1:
@@ -291,7 +291,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 (* Not used since applic_prs proves a version for an arbitrary number of arguments *)
@@ -300,7 +300,7 @@
   and     q2: "Quotient R2 abs2 rep2"
   shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
@@ -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,           *)
@@ -347,7 +347,7 @@
 lemma IF_PRS:
   assumes q: "Quotient R Abs Rep"
   shows "If a b c = Abs (If a (Rep b) (Rep c))"
-using Quotient_ABS_REP[OF q] by auto
+using Quotient_abs_rep[OF q] by auto
 
 (* ask peter: no use of q *)
 lemma IF_RSP:
@@ -360,7 +360,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
 
 lemma LET_RSP:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -384,7 +384,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
 
 (* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
@@ -408,7 +408,7 @@
 lemma I_PRS:
   assumes q: "Quotient R Abs Rep"
   shows "id e = Abs (id (Rep e))"
-using Quotient_ABS_REP[OF q] by auto
+using Quotient_abs_rep[OF q] by auto
 
 lemma I_RSP:
   assumes q: "Quotient R Abs Rep"
@@ -421,7 +421,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   and     q3: "Quotient R3 Abs3 Rep3"
   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
 unfolding o_def expand_fun_eq
 by simp