diff -r a19a5179fbca -r 44fa9df44e6f QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -130,16 +130,16 @@
 by (simp add: mem_def)
 
 fun
-  FUN_REL 
+  fun_rel
 where
-  "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 abbreviation
-  FUN_REL_syn (infixr "===>" 55)
+  fun_rel_syn (infixr "===>" 55)
 where
-  "E1 ===> E2 \<equiv> FUN_REL E1 E2"
+  "E1 ===> E2 \<equiv> fun_rel E1 E2"
 
-lemma FUN_REL_EQ:
+lemma fun_rel_eq:
   "(op =) ===> (op =) \<equiv> (op =)"
 by (rule eq_reflection) (simp add: expand_fun_eq)
 
@@ -219,7 +219,7 @@
                           (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
 *)
 
-lemma FUN_REL_EQ_REL:
+lemma fun_rel_EQ_REL:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
@@ -229,17 +229,17 @@
 
 (* TODO: it is the same as APPLY_RSP *)
 (* q1 and q2 not used; see next lemma *)
-lemma FUN_REL_MP:
+lemma fun_rel_MP:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 by simp
 
-lemma FUN_REL_IMP:
+lemma fun_rel_IMP:
   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 by simp
 
-lemma FUN_REL_EQUALS:
+lemma fun_rel_EQUALS:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     r1: "Respects (R1 ===> R2) f"
@@ -247,14 +247,14 @@
   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 apply(rule_tac iffI)
 using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-apply(metis FUN_REL_IMP)
+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])
 done
 
-(* ask Peter: FUN_REL_IMP used twice *) 
-lemma FUN_REL_IMP2:
+(* ask Peter: fun_rel_IMP used twice *) 
+lemma fun_rel_IMP2:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     r1: "Respects (R1 ===> R2) f"
@@ -262,7 +262,7 @@
   and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
   shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
 using q1 q2 r1 r2 a
-by (simp add: FUN_REL_EQUALS)
+by (simp add: fun_rel_EQUALS)
 
 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *)
 lemma EQUALS_PRS:
@@ -367,7 +367,7 @@
   and     a1: "(R1 ===> R2) f g"
   and     a2: "R1 x y"
   shows "R2 (Let x f) (Let y g)"
-using FUN_REL_MP[OF q1 q2 a1] a2
+using fun_rel_MP[OF q1 q2 a1] a2
 by auto
 
 
@@ -393,12 +393,12 @@
   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)
+using a by (rule fun_rel_IMP)
 
 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)
+using a by (rule fun_rel_IMP)
 
 
 (* combinators: I, K, o, C, W *)