--- a/Quot/QuotScript.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -126,30 +126,19 @@
   using a unfolding Quotient_def transp_def
   by metis
 
-fun
-  fun_map
+definition
+  fun_map (infixr "--->" 55)
 where
-  "fun_map f g h x = g (h (f x))"
-
-abbreviation
-  fun_map_syn (infixr "--->" 55)
-where
-  "f ---> g \<equiv> fun_map f g"
+[simp]: "fun_map f g h x = g (h (f x))"
 
 lemma fun_map_id:
   shows "(id ---> id) = id"
   by (simp add: expand_fun_eq id_def)
 
-
-fun
-  fun_rel
+definition
+  fun_rel (infixr "===>" 55)
 where
-  "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
-
-abbreviation
-  fun_rel_syn (infixr "===>" 55)
-where
-  "E1 ===> E2 \<equiv> fun_rel E1 E2"
+[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 lemma fun_rel_eq:
   "(op =) ===> (op =) \<equiv> (op =)"
@@ -453,18 +442,18 @@
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
 
-(* 2 lemmas needed for cleaning of quantifiers *)
+(* 3 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
-  using a unfolding Quotient_def
-  by (metis in_respects fun_map.simps id_apply)
+  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+by metis
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
-  using a unfolding Quotient_def
-  by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
+  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+  by metis
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
@@ -639,8 +628,13 @@
   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)
+  apply(rule)+
+  apply (rule apply_rsp'[of "R1" "R2"])
+  apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
+  apply auto
   using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-  apply(metis apply_rsp')
+  apply (metis let_rsp q1)
+  apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
   using r1 unfolding Respects_def expand_fun_eq
   apply(simp (no_asm_use))
   apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])