diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -17,6 +17,16 @@
   "~~/src/HOL/Library/Multiset"
 begin
 
+notation
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90) and
+  convol ("<_ , _>")
+
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
@@ -84,7 +94,7 @@
   thus "map f x = map g x" by simp
 next
   fix f
-  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
+  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
 next
   show "card_order natLeq" by (rule natLeq_card_order)
 next
@@ -237,7 +247,7 @@
   also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
-    by transfer (unfold o_apply, blast)
+    by transfer (unfold comp_apply, blast)
 qed
 
 lemma mmap_cong:
@@ -255,7 +265,7 @@
 end
 
 lemma set_of_mmap: "set_of o mmap h = image h o set_of"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
   fix M show "set_of (mmap h M) = h ` set_of M"
     by transfer (auto simp add: multiset_def setsum_gt_0_iff)
 qed
@@ -687,7 +697,7 @@
         case True
         def c \<equiv> "f1 b1"
         have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
-          unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
@@ -723,7 +733,7 @@
         case True
         def c \<equiv> "f2 b2"
         have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
-          unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
@@ -738,7 +748,7 @@
           apply(rule setsum_reindex)
           using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
         also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
-        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
+        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
           apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
           using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
         finally show ?thesis .
@@ -762,7 +772,7 @@
     by (blast dest: wppull_thePull)
   then show ?thesis
     by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
-      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
+      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
         intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
 qed
 
@@ -774,7 +784,7 @@
 by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   Grp_def relcompp.simps intro: mmap_cong)
   (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
-    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
+    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
 
 inductive rel_multiset' where
   Zero[intro]: "rel_multiset' R {#} {#}"