Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished replacing OO by OOO
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 12 Jan 2010 16:44:33 +0100
changeset 852 67e5da3a356a
parent 851 e1473b4b2886
child 853 3fd1365f5729
Finished replacing OO by OOO
Quot/Examples/AbsRepTest.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2