--- 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 :