--- a/QuotScript.thy	Fri Dec 04 14:11:20 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 14:35:36 2009 +0100
@@ -266,14 +266,14 @@
   shows "(x = y) = R (Rep x) (Rep y)"
 by (rule QUOTIENT_REL_REP[OF q, symmetric])
 
-lemma EQUALS_RSP:
+lemma equals_rsp:
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R xa xb" "R ya yb"
   shows "R xa ya = R xb yb"
 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
 using a by blast
 
-lemma LAMBDA_PRS:
+lemma lambda_prs:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
   and     q2: "QUOTIENT R2 Abs2 Rep2"
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
@@ -281,10 +281,10 @@
 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
 by simp
 
-lemma LAMBDA_PRS1:
+lemma lambda_prs1:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
   and     q2: "QUOTIENT R2 Abs2 Rep2"
-  shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
+  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]
 by simp
@@ -334,7 +334,7 @@
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
-(*              RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
+(*              Ball, Bex, RES_EXISTS_EQUIV              *)
 (* ----------------------------------------------------- *)
 
 (* bool theory: COND, LET *)
@@ -374,32 +374,24 @@
 
 (* FUNCTION APPLICATION *)
 
+(* Not used *)
 lemma APPLY_PRS:
   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
 
-(* ask peter: no use of q1 q2 *)
-(* Cez: I can answer,
-   In the following theorem R2 can be instantiated with anything,
+(* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
    so by solving QUOTIENT assumptions we can get a unique R2 that
-   will be provable; which is why we need to use APPLY_RSP1 *)
-lemma APPLY_RSP:
-  assumes q1: "QUOTIENT R1 Abs1 Rep1"
-  and     q2: "QUOTIENT R2 Abs2 Rep2"
-  and     a: "(R1 ===> R2) f g" "R1 x y"
-  shows "R2 (f x) (g y)"
-using a by (rule FUN_REL_IMP)
-
-lemma APPLY_RSP1:
+   will be provable; which is why we need to use APPLY_RSP *)
+lemma apply_rsp:
   assumes q: "QUOTIENT R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
 using a by (rule FUN_REL_IMP)
 
-lemma APPLY_RSP2:
+lemma apply_rsp':
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
 using a by (rule FUN_REL_IMP)