--- a/QuotScript.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -121,11 +121,12 @@
 where
   "f ---> g \<equiv> fun_map f g"
 
-lemma FUN_MAP_I:
+lemma fun_map_id:
   shows "(id ---> id) = id"
 by (simp add: expand_fun_eq id_def)
 
-lemma IN_FUN:
+(* Not used *)
+lemma in_fun:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
 by (simp add: mem_def)
 
@@ -143,7 +144,7 @@
   "(op =) ===> (op =) \<equiv> (op =)"
 by (rule eq_reflection) (simp add: expand_fun_eq)
 
-lemma FUN_Quotient:
+lemma fun_quotient:
   assumes q1: "Quotient R1 abs1 rep1"
   and     q2: "Quotient R2 abs2 rep2"
   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
@@ -224,7 +225,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
-using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
+using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
 by blast
 
 (* TODO: it is the same as APPLY_RSP *)
@@ -246,7 +247,7 @@
   and     r2: "Respects (R1 ===> R2) g" 
   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
+using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))