--- a/Quot/Examples/FSet3.thy	Tue Jan 12 16:21:42 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Tue Jan 12 16:28:53 2010 +0100
@@ -254,10 +254,10 @@
 by (simp add: id_simps)
 
 lemma concat_rsp[quot_respect]:
-  shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
+  shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 sorry
 
-lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
+lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
   done
 
@@ -272,9 +272,8 @@
   done
 
 lemma quotient_compose_list_pre:
-  "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s =
-  ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and>
-  (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and>
+  "(list_rel op \<approx> OOO op \<approx>) r s =
+  ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>
   abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
   apply rule
   apply rule
@@ -323,8 +322,8 @@
   done
 
 lemma quotient_compose_list[quot_thm]:
-  shows  "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>))
-  (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+  shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
+    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
   apply (rule)+
   apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
@@ -354,7 +353,7 @@
 (* Should be true *)
 
 lemma insert_rsp2[quot_respect]:
-  "(op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) op # op #"
+  "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
 apply auto
 apply (simp add: set_in_eq)
 sorry