# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263311073 -3600
# Node ID 67e5da3a356a752f364bda802145a5ba85c8046a
# Parent  e1473b4b288680b71eb28d91abef0149051a1727
Finished replacing OO by OOO

diff -r e1473b4b2886 -r 67e5da3a356a Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 12 16:28:53 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 12 16:44:33 2010 +0100
@@ -145,9 +145,8 @@
 lemma quotient_compose_list_gen_pre:
   assumes a: "equivp r2"
   and b: "Quotient r2 abs2 rep2"
-  shows  "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s =
-          ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and>
-           (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and>
+  shows  "(list_rel r2 OOO op \<approx>1) r s =
+          ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and>
            abs_fset (map abs2 r) = abs_fset (map abs2 s))"
   apply rule
   apply rule
@@ -199,7 +198,7 @@
 lemma quotient_compose_list_gen:
   assumes a: "Quotient r2 abs2 rep2"
   and     b: "equivp r2" (* reflp is not enough *)
-  shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2))
+  shows  "Quotient ((list_rel r2) OOO (op \<approx>1))
                (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
   apply (rule)+
@@ -223,7 +222,7 @@
 lemma quotient_compose_general:
   assumes a2: "Quotient r1 abs1 rep1"
   and         "Quotient r2 abs2 rep2"
-  shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2))
+  shows  "Quotient ((list_rel r2) OOO r1)
                (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
 sorry