--- a/QuotScript.thy	Sat Oct 24 10:16:53 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 13:00:54 2009 +0200
@@ -127,7 +127,7 @@
   "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"  
 
@@ -509,6 +509,7 @@
   shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
   sorry
 
+(* Currently fixed, should be general *)
 lemma ho_all_prs: "op = ===> op = ===> op = All All"
   apply (auto)
   done