--- a/FSet.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/FSet.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -183,7 +183,7 @@
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
+lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
 lemma cons_rsp:
@@ -193,7 +193,7 @@
   using a by (rule list_eq.intros(5))
 
 lemma ho_cons_rsp:
-  "op = ===> op \<approx> ===> op \<approx> op # op #"
+  "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
 lemma append_rsp_fst:
@@ -250,7 +250,7 @@
   done
 
 lemma ho_append_rsp:
-  "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
 lemma map_rsp:
@@ -262,7 +262,7 @@
   done
 
 lemma fun_rel_id:
-  "op = ===> op = \<equiv> op ="
+  "(op = ===> op =) \<equiv> op ="
   apply (rule eq_reflection)
   apply (rule ext)
   apply (rule ext)
@@ -273,7 +273,7 @@
   done
 
 lemma ho_map_rsp:
-  "op = ===> op = ===> op \<approx> ===> op \<approx> map map"
+  "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: fun_rel_id map_rsp)
 
 lemma map_append :

--- a/IntEx.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -111,7 +111,7 @@
   done
 
 lemma ho_plus_rsp:
-  "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
+  "(intrel ===> intrel ===> intrel) my_plus my_plus"
   by (simp)
 
 ML {* val consts = [@{const_name "my_plus"}] *}

--- a/LamEx.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -43,9 +43,9 @@
 
 (* Construction Site code *)
 
-lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" sorry
-lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" sorry
-lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" sorry
+lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" sorry
+lemma fresh_rsp: "(op = ===> (alpha ===> op =)) fresh fresh" sorry
+lemma rLam_rsp: "(op = ===> (alpha ===> alpha)) rLam rLam" sorry
 
 ML {* val defs = @{thms Var_def App_def Lam_def} *}
 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *}
@@ -91,7 +91,4 @@
 ML {* ObjectLogic.rulify t_b' *}
 
 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
-lemma "alpha ===> (alpha ===> op =) op = op ="
-sorry
-
 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *)

--- a/QuotScript.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/QuotScript.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -131,9 +131,9 @@
   "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 abbreviation
-  FUN_REL_syn ("_ ===> _")
+  FUN_REL_syn (infixr "===>" 55)
 where
-  "E1 ===> E2 \<equiv> FUN_REL E1 E2"  
+  "E1 ===> E2 \<equiv> FUN_REL E1 E2"
 
 lemma FUN_REL_EQ:
   "(op =) ===> (op =) = (op =)"
@@ -512,11 +512,11 @@
 
 (* These are the fixed versions, general ones need to be proved. *)
 lemma ho_all_prs:
-  shows "op = ===> op = ===> op = All All"
+  shows "((op = ===> op =) ===> op =) All All"
   by auto
 
-lemma ho_ex_prs: 
-  shows "op = ===> op = ===> op = Ex Ex"
+lemma ho_ex_prs:
+  shows "((op = ===> op =) ===> op =) Ex Ex"
   by auto
 
 end