# HG changeset patch
# User wenzelm
# Date 1451655892 -3600
# Node ID ea3b1b0413b40e432daa0eb28914a8eaa0ef1770
# Parent  8007e4ff493aa3bc603b2b2e7869db45095df628
more symbols;

diff -r 8007e4ff493a -r ea3b1b0413b4 NEWS
--- a/NEWS	Fri Jan 01 11:27:29 2016 +0100
+++ b/NEWS	Fri Jan 01 14:44:52 2016 +0100
@@ -598,6 +598,8 @@
 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
 "top". INCOMPATIBILITY.
 
+* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
+
 * Library/Multiset:
   - Renamed multiset inclusion operators:
       < ~> <#
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -338,7 +338,7 @@
   using assms by (rule effectE) (simp add: execute_simps)
 
 lemma upd_return:
-  "upd i x a \<guillemotright> return a = upd i x a"
+  "upd i x a \<then> return a = upd i x a"
   by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
 
 lemma array_make:
@@ -371,10 +371,10 @@
   by (simp add: make'_def o_def)
 
 definition len' where
-  [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (of_nat n))"
+  [code del]: "len' a = Array.len a \<bind> (\<lambda>n. return (of_nat n))"
 
 lemma [code]:
-  "Array.len a = len' a \<guillemotright>= (\<lambda>i. return (nat_of_integer i))"
+  "Array.len a = len' a \<bind> (\<lambda>i. return (nat_of_integer i))"
   by (simp add: len'_def)
 
 definition nth' where
@@ -385,10 +385,10 @@
   by (simp add: nth'_def)
 
 definition upd' where
-  [code del]: "upd' a i x = Array.upd (nat_of_integer i) x a \<guillemotright> return ()"
+  [code del]: "upd' a i x = Array.upd (nat_of_integer i) x a \<then> return ()"
 
 lemma [code]:
-  "Array.upd i x a = upd' a (of_nat i) x \<guillemotright> return a"
+  "Array.upd i x a = upd' a (of_nat i) x \<then> return a"
   by (simp add: upd'_def upd_return)
 
 lemma [code]:
@@ -497,4 +497,3 @@
 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
 
 end
-
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -253,56 +253,56 @@
   Monad_Syntax.bind Heap_Monad.bind
 
 lemma execute_bind [execute_simps]:
-  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
-  "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
+  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<bind> g) h = execute (g x) h'"
+  "execute f h = None \<Longrightarrow> execute (f \<bind> g) h = None"
   by (simp_all add: bind_def)
 
 lemma execute_bind_case:
-  "execute (f \<guillemotright>= g) h = (case (execute f h) of
+  "execute (f \<bind> g) h = (case (execute f h) of
     Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
   by (simp add: bind_def)
 
 lemma execute_bind_success:
-  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
+  "success f h \<Longrightarrow> execute (f \<bind> g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
 
 lemma success_bind_executeI:
-  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
   by (auto intro!: successI elim: successE simp add: bind_def)
 
 lemma success_bind_effectI [success_intros]:
-  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
   by (auto simp add: effect_def success_def bind_def)
 
 lemma effect_bindI [effect_intros]:
   assumes "effect f h h' r" "effect (g r) h' h'' r'"
-  shows "effect (f \<guillemotright>= g) h h'' r'"
+  shows "effect (f \<bind> g) h h'' r'"
   using assms
   apply (auto intro!: effectI elim!: effectE successE)
   apply (subst execute_bind, simp_all)
   done
 
 lemma effect_bindE [effect_elims]:
-  assumes "effect (f \<guillemotright>= g) h h'' r'"
+  assumes "effect (f \<bind> g) h h'' r'"
   obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
   using assms by (auto simp add: effect_def bind_def split: option.split_asm)
 
 lemma execute_bind_eq_SomeI:
   assumes "execute f h = Some (x, h')"
     and "execute (g x) h' = Some (y, h'')"
-  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
+  shows "execute (f \<bind> g) h = Some (y, h'')"
   using assms by (simp add: bind_def)
 
-lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
+lemma return_bind [simp]: "return x \<bind> f = f x"
   by (rule Heap_eqI) (simp add: execute_simps)
 
-lemma bind_return [simp]: "f \<guillemotright>= return = f"
+lemma bind_return [simp]: "f \<bind> return = f"
   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
-lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: 'a Heap) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
+lemma bind_bind [simp]: "(f \<bind> g) \<bind> k = (f :: 'a Heap) \<bind> (\<lambda>x. g x \<bind> k)"
   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
-lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
+lemma raise_bind [simp]: "raise e \<bind> f = raise e"
   by (rule Heap_eqI) (simp add: execute_simps)
 
 
@@ -334,7 +334,7 @@
 lemma assert_cong [fundef_cong]:
   assumes "P = P'"
   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
-  shows "(assert P x >>= f) = (assert P' x >>= f')"
+  shows "(assert P x \<bind> f) = (assert P' x \<bind> f')"
   by (rule Heap_eqI) (insert assms, simp add: assert_def)
 
 
@@ -348,7 +348,7 @@
   by (simp add: lift_def)
 
 lemma bind_lift:
-  "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
+  "(f \<bind> lift g) = (f \<bind> (\<lambda>x. return (g x)))"
   by (simp add: lift_def comp_def)
 
 
@@ -363,7 +363,7 @@
    }"
 
 lemma fold_map_append:
-  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
+  "fold_map f (xs @ ys) = fold_map f xs \<bind> (\<lambda>xs. fold_map f ys \<bind> (\<lambda>ys. return (xs @ ys)))"
   by (induct xs) simp_all
 
 lemma execute_fold_map_unchanged_heap [execute_simps]:
@@ -476,7 +476,7 @@
 
 lemma bind_mono [partial_function_mono]:
   assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
-  shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
+  shows "mono_Heap (\<lambda>f. B f \<bind> (\<lambda>y. C y f))"
 proof (rule monotoneI)
   fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
   from mf
@@ -484,7 +484,7 @@
   from mg
   have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
 
-  have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
+  have "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))"
     (is "Heap_ord ?L ?R")
   proof (rule Heap_ordI)
     fix h
@@ -492,7 +492,7 @@
       by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
   qed
   also
-  have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
+  have "Heap_ord (B g \<bind> (\<lambda>y'. C y' f)) (B g \<bind> (\<lambda>y'. C y' g))"
     (is "Heap_ord ?L ?R")
   proof (rule Heap_ordI)
     fix h
@@ -512,7 +512,7 @@
     qed
   qed
   finally (heap.leq_trans)
-  show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
+  show "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))" .
 qed
 
 
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -208,11 +208,11 @@
   using assms by (rule effectE) (simp add: execute_simps)
 
 lemma lookup_chain:
-  "(!r \<guillemotright> f) = f"
+  "(!r \<then> f) = f"
   by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
 
 lemma update_change [code]:
-  "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
+  "r := e = change (\<lambda>_. e) r \<then> return ()"
   by (rule Heap_eqI) (simp add: change_def lookup_chain)
 
 
@@ -320,4 +320,3 @@
 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
 
 end
-
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -601,12 +601,12 @@
 lemma success_bindI' [success_intros]: (*FIXME move*)
   assumes "success f h"
   assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
-  shows "success (f \<guillemotright>= g) h"
+  shows "success (f \<bind> g) h"
 using assms(1) proof (rule success_effectE)
   fix h' r
   assume *: "effect f h h' r"
   with assms(2) have "success (g r) h'" .
-  with * show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
+  with * show "success (f \<bind> g) h" by (rule success_bind_effectI)
 qed
 
 lemma success_partitionI:
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -110,7 +110,7 @@
       subarray_def rev.simps[where j=0] elim!: effect_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
-definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
+definition "example = (Array.make 10 id \<bind> (\<lambda>a. rev a 0 9))"
 
 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -507,7 +507,7 @@
 qed
 
 lemma traverse_make_llist':
-  assumes effect: "effect (make_llist xs \<guillemotright>= traverse) h h' r"
+  assumes effect: "effect (make_llist xs \<bind> traverse) h h' r"
   shows "r = xs"
 proof -
   from effect obtain h1 r1
@@ -942,8 +942,8 @@
 
 text {* A simple example program *}
 
-definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
-definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
+definition test_1 where "test_1 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; xs \<leftarrow> traverse ll_xs; return xs })" 
+definition test_2 where "test_2 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; ll_ys \<leftarrow> rev ll_xs; ys \<leftarrow> traverse ll_ys; return ys })"
 
 definition test_3 where "test_3 =
   (do {
@@ -966,4 +966,3 @@
 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
-
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -201,9 +201,9 @@
   "res_thm' l (x#xs) (y#ys) = 
   (if (x = l \<or> x = compl l) then resolve2 (compl x) xs (y#ys)
   else (if (y = l \<or> y = compl l) then resolve1 (compl y) (x#xs) ys
-  else (if (x < y) then (res_thm' l xs (y#ys)) \<guillemotright>= (\<lambda>v. return (x # v))
-  else (if (x > y) then (res_thm' l (x#xs) ys) \<guillemotright>= (\<lambda>v. return (y # v))
-  else (res_thm' l xs ys) \<guillemotright>= (\<lambda>v. return (x # v))))))"
+  else (if (x < y) then (res_thm' l xs (y#ys)) \<bind> (\<lambda>v. return (x # v))
+  else (if (x > y) then (res_thm' l (x#xs) ys) \<bind> (\<lambda>v. return (y # v))
+  else (res_thm' l xs ys) \<bind> (\<lambda>v. return (x # v))))))"
 | "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
 | "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
 
@@ -432,7 +432,7 @@
   foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
 where
   "foldM f [] s = return s"
-  | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
+  | "foldM f (x#xs) s = f x s \<bind> foldM f xs"
 
 fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
 where
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -15,28 +15,22 @@
 \<close>
 
 consts
-  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<guillemotright>=" 54)
+  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
 
 notation (ASCII)
   bind (infixr ">>=" 54)
 
-notation (latex output)
-  bind (infixr "\<bind>" 54)
-
 
 abbreviation (do_notation)
   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
   where "bind_do \<equiv> bind"
 
 notation (output)
-  bind_do (infixr "\<guillemotright>=" 54)
+  bind_do (infixr "\<bind>" 54)
 
 notation (ASCII output)
   bind_do (infixr ">>=" 54)
 
-notation (latex output)
-  bind_do (infixr "\<bind>" 54)
-
 
 nonterminal do_binds and do_bind
 syntax
@@ -46,15 +40,12 @@
   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
 
 syntax (ASCII)
   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
 
-syntax (latex output)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
-
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"
     == "CONST bind_do t (\<lambda>_. e)"
@@ -67,7 +58,7 @@
   "_do_cons (_do_let p t) (_do_final s)"
     == "_do_final (let p = t in s)"
   "_do_block (_do_final e)" => "e"
-  "(m >> n)" => "(m >>= (\<lambda>_. n))"
+  "(m \<then> n)" => "(m \<bind> (\<lambda>_. n))"
 
 adhoc_overloading
   bind Set.bind Predicate.bind Option.bind List.bind
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Predicate.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -120,35 +120,35 @@
   "eval (single x) = (op =) x"
   by (simp add: single_def)
 
-definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
-  "P \<guillemotright>= f = (SUPREMUM {x. eval P x} f)"
+definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where
+  "P \<bind> f = (SUPREMUM {x. eval P x} f)"
 
 lemma eval_bind [simp]:
-  "eval (P \<guillemotright>= f) = eval (SUPREMUM {x. eval P x} f)"
+  "eval (P \<bind> f) = eval (SUPREMUM {x. eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind:
-  "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
+  "(P \<bind> Q) \<bind> R = P \<bind> (\<lambda>x. Q x \<bind> R)"
   by (rule pred_eqI) auto
 
 lemma bind_single:
-  "P \<guillemotright>= single = P"
+  "P \<bind> single = P"
   by (rule pred_eqI) auto
 
 lemma single_bind:
-  "single x \<guillemotright>= P = P x"
+  "single x \<bind> P = P x"
   by (rule pred_eqI) auto
 
 lemma bottom_bind:
-  "\<bottom> \<guillemotright>= P = \<bottom>"
+  "\<bottom> \<bind> P = \<bottom>"
   by (rule pred_eqI) auto
 
 lemma sup_bind:
-  "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
+  "(P \<squnion> Q) \<bind> R = P \<bind> R \<squnion> Q \<bind> R"
   by (rule pred_eqI) auto
 
 lemma Sup_bind:
-  "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
+  "(\<Squnion>A \<bind> f) = \<Squnion>((\<lambda>x. x \<bind> f) ` A)"
   by (rule pred_eqI) auto
 
 lemma pred_iffI:
@@ -169,10 +169,10 @@
 lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
-lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
+lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<bind> Q) y"
   by auto
 
-lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
+lemma bindE: "eval (R \<bind> Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   by auto
 
 lemma botE: "eval \<bottom> x \<Longrightarrow> P"
@@ -401,7 +401,7 @@
 by (rule unit_pred_cases) (auto elim: botE intro: singleI)
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
-  "map f P = P \<guillemotright>= (single o f)"
+  "map f P = P \<bind> (single o f)"
 
 lemma eval_map [simp]:
   "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
@@ -455,11 +455,11 @@
 
 primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   "apply f Empty = Empty"
-| "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
-| "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
+| "apply f (Insert x P) = Join (f x) (Join (P \<bind> f) Empty)"
+| "apply f (Join P xq) = Join (P \<bind> f) (apply f xq)"
 
 lemma apply_bind:
-  "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
+  "pred_of_seq (apply f xq) = pred_of_seq xq \<bind> f"
 proof (induct xq)
   case Empty show ?case
     by (simp add: bottom_bind)
@@ -472,7 +472,7 @@
 qed
   
 lemma bind_code [code]:
-  "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
+  "Seq g \<bind> f = Seq (\<lambda>u. apply f (g ()))"
   unfolding Seq_def by (rule sym, rule apply_bind)
 
 lemma bot_set_code [code]:
@@ -727,7 +727,7 @@
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
 no_notation
-  bind (infixl "\<guillemotright>=" 70)
+  bind (infixl "\<bind>" 70)
 
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -1107,13 +1107,13 @@
 
 lemma emeasure_bind:
     "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
-      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+      \<Longrightarrow> emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
 
 lemma nn_integral_bind:
   assumes f: "f \<in> borel_measurable B"
   assumes N: "N \<in> measurable M (subprob_algebra B)"
-  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
 proof cases
   assume M: "space M \<noteq> {}" show ?thesis
     unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
@@ -1123,17 +1123,17 @@
 lemma AE_bind:
   assumes P[measurable]: "Measurable.pred B P"
   assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
-  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
+  shows "(AE x in M \<bind> N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
 proof cases
   assume M: "space M = {}" show ?thesis
     unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
 next
   assume M: "space M \<noteq> {}"
   note sets_kernel[OF N, simp]
-  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
+  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<bind> N))"
     by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
 
-  have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
+  have "(AE x in M \<bind> N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
     by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
              del: nn_integral_indicator)
   also have "\<dots> = (AE x in M. AE y in N x. P y)"
@@ -1180,9 +1180,9 @@
 
 lemma subprob_space_bind:
   assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
-  shows "subprob_space (M \<guillemotright>= f)"
-proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
-  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
+  shows "subprob_space (M \<bind> f)"
+proof (rule subprob_space_kernel[of "\<lambda>x. x \<bind> f"])
+  show "(\<lambda>x. x \<bind> f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
     by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
         rule measurable_compose[OF measurable_snd assms(2)])
   from assms(1) show "M \<in> space (subprob_algebra M)"
@@ -1218,27 +1218,27 @@
 lemma (in prob_space) prob_space_bind: 
   assumes ae: "AE x in M. prob_space (N x)"
     and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
-  shows "prob_space (M \<guillemotright>= N)"
+  shows "prob_space (M \<bind> N)"
 proof
-  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
+  have "emeasure (M \<bind> N) (space (M \<bind> N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
     by (subst emeasure_bind[where N=S])
        (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
   also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
     using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
-  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
+  finally show "emeasure (M \<bind> N) (space (M \<bind> N)) = 1"
     by (simp add: emeasure_space_1)
 qed
 
 lemma (in subprob_space) bind_in_space:
-  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
+  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<bind> A) \<in> space (subprob_algebra N)"
   by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
      unfold_locales
 
 lemma (in subprob_space) measure_bind:
   assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
-  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
+  shows "measure (M \<bind> f) X = \<integral>x. measure (f x) X \<partial>M"
 proof -
-  interpret Mf: subprob_space "M \<guillemotright>= f"
+  interpret Mf: subprob_space "M \<bind> f"
     by (rule subprob_space_bind[OF _ f]) unfold_locales
 
   { fix x assume "x \<in> space M"
@@ -1248,7 +1248,7 @@
       by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
   note this[simp]
 
-  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+  have "emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
     using subprob_not_empty f X by (rule emeasure_bind)
   also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
     by (intro nn_integral_cong) simp
@@ -1262,29 +1262,29 @@
 
 lemma emeasure_bind_const: 
     "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
-         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+         emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
   by (simp add: bind_nonempty emeasure_join nn_integral_distr 
                 space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
 
 lemma emeasure_bind_const':
   assumes "subprob_space M" "subprob_space N"
-  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+  shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
 using assms
 proof (case_tac "X \<in> sets N")
   fix X assume "X \<in> sets N"
-  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
+  thus "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
       by (subst emeasure_bind_const) 
          (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
 next
   fix X assume "X \<notin> sets N"
-  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+  with assms show "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
       by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
                     space_subprob_algebra emeasure_notin_sets)
 qed
 
 lemma emeasure_bind_const_prob_space:
   assumes "prob_space M" "subprob_space N"
-  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
+  shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X"
   using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
                             prob_space.emeasure_space_1)
 
@@ -1304,7 +1304,7 @@
 lemma distr_bind:
   assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}"
   assumes f: "f \<in> measurable K R"
-  shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))"
+  shows "distr (M \<bind> N) R f = (M \<bind> (\<lambda>x. distr (N x) R f))"
   unfolding bind_nonempty''[OF N]
   apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)])
   apply (rule f)
@@ -1316,7 +1316,7 @@
 lemma bind_distr:
   assumes f[measurable]: "f \<in> measurable M X"
   assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}"
-  shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))"
+  shows "(distr M X f \<bind> N) = (M \<bind> (\<lambda>x. N (f x)))"
 proof -
   have "space X \<noteq> {}" "space M \<noteq> {}"
     using \<open>space M \<noteq> {}\<close> f[THEN measurable_space] by auto
@@ -1326,12 +1326,12 @@
 
 lemma bind_count_space_singleton:
   assumes "subprob_space (f x)"
-  shows "count_space {x} \<guillemotright>= f = f x"
+  shows "count_space {x} \<bind> f = f x"
 proof-
   have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
   have "count_space {x} = return (count_space {x}) x"
     by (intro measure_eqI) (auto dest: A)
-  also have "... \<guillemotright>= f = f x"
+  also have "... \<bind> f = f x"
     by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
   finally show ?thesis .
 qed
@@ -1346,10 +1346,10 @@
   note N_space = sets_eq_imp_space_eq[OF N_sets, simp]
   show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))"
     by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]])
-  fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
+  fix A assume "A \<in> sets (restrict_space (M \<bind> N) X)"
   with X have "A \<in> sets K" "A \<subseteq> X"
     by (auto simp: sets_restrict_space)
-  then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
+  then show "emeasure (restrict_space (M \<bind> N) X) A = emeasure (M \<bind> (\<lambda>x. restrict_space (N x) X)) A"
     using assms
     apply (subst emeasure_restrict_space)
     apply (simp_all add: emeasure_bind[OF assms(2,1)])
@@ -1362,8 +1362,8 @@
 lemma bind_restrict_space:
   assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M"
   and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)"
-  shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
-  (is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f")
+  shows "restrict_space M A \<bind> f = M \<bind> (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
+  (is "?lhs = ?rhs" is "_ = M \<bind> ?f")
 proof -
   let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M"
   let ?x = "Eps ?P"
@@ -1391,7 +1391,7 @@
   finally show ?thesis .
 qed
 
-lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
+lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<bind> (\<lambda>x. N) = N"
   by (intro measure_eqI) 
      (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
 
@@ -1445,15 +1445,15 @@
   assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   assumes Mf: "f \<in> measurable M (subprob_algebra M')"
   assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N"
-  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
+  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g"
 proof-
-  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
-            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}"
+  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g = 
+            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g}"
     using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg
                       measurable_compose[OF _ return_measurable] simp: measurable_split_conv)
   also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable
-  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 
-            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}"
+  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g} = 
+            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g}"
     apply (intro ballI bind_cong bind_assoc)
     apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp)
     apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg)
@@ -1461,7 +1461,7 @@
   also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'"
     by (intro sets_eq_imp_space_eq sets_kernel[OF Mf])
   with measurable_space[OF Mh] 
-    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
+    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
     by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
   finally show ?thesis ..
 qed
@@ -1470,36 +1470,36 @@
   by (simp add: space_subprob_algebra) unfold_locales
 
 lemma (in pair_prob_space) pair_measure_eq_bind:
-  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
 proof (rule measure_eqI)
   have ps_M2: "prob_space M2" by unfold_locales
   note return_measurable[measurable]
-  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
     by (simp_all add: M1.not_empty M2.not_empty)
   fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
-  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
+  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
     by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"]
              intro!: nn_integral_cong)
 qed
 
 lemma (in pair_prob_space) bind_rotate:
   assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)"
-  shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+  shows "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))"
 proof - 
   interpret swap: pair_prob_space M2 M1 by unfold_locales
   note measurable_bind[where N="M2", measurable]
   note measurable_bind[where N="M1", measurable]
   have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)"
     by (auto simp: space_subprob_algebra) unfold_locales
-  have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 
-    (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+  have "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = 
+    (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<bind> (\<lambda>(x, y). C x y)"
     by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N])
-  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<bind> (\<lambda>(x, y). C x y)"
     unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] ..
-  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)"
+  also have "\<dots> = (M2 \<bind> (\<lambda>x. M1 \<bind> (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<bind> (\<lambda>(y, x). C x y)"
     unfolding swap.pair_measure_eq_bind[symmetric]
     by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong)
-  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+  also have "\<dots> = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))"
     by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N])
   finally show ?thesis .
 qed
@@ -1552,7 +1552,7 @@
     by (simp add: emeasure_notin_sets)
 qed
 
-lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
+lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<bind> return N = M"
    by (cases "space M = {}")
       (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
                 cong: subprob_algebra_cong)
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -334,13 +334,13 @@
   assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
   shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
 proof (rule measure_eqI)
-  show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
+  show "sets (measure_pmf x \<bind> A) = sets (measure_pmf x \<bind> B)"
     using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
 next
-  fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
+  fix X assume "X \<in> sets (measure_pmf x \<bind> A)"
   then have X: "X \<in> sets N"
     using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
-  show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
+  show "emeasure (measure_pmf x \<bind> A) X = emeasure (measure_pmf x \<bind> B) X"
     using assms
     by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
        (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
@@ -362,13 +362,13 @@
   have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
     by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
 
-  show "prob_space (f \<guillemotright>= g)"
+  show "prob_space (f \<bind> g)"
     using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
-  then interpret fg: prob_space "f \<guillemotright>= g" .
-  show [simp]: "sets (f \<guillemotright>= g) = UNIV"
+  then interpret fg: prob_space "f \<bind> g" .
+  show [simp]: "sets (f \<bind> g) = UNIV"
     using sets_eq_imp_space_eq[OF s_f]
     by (subst sets_bind[where N="count_space UNIV"]) auto
-  show "AE x in f \<guillemotright>= g. measure (f \<guillemotright>= g) {x} \<noteq> 0"
+  show "AE x in f \<bind> g. measure (f \<bind> g) {x} \<noteq> 0"
     apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"])
     using ae_f
     apply eventually_elim
@@ -408,7 +408,7 @@
   "p = q \<Longrightarrow> (\<And>x. x \<in> set_pmf q =simp=> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
   by (simp add: simp_implies_def cong: bind_pmf_cong)
 
-lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
+lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<bind> (\<lambda>x. measure_pmf (f x)))"
   by transfer simp
 
 lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
@@ -437,7 +437,7 @@
 
 lemma bind_return_pmf': "bind_pmf N return_pmf = N"
 proof (transfer, clarify)
-  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
+  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<bind> return (count_space UNIV) = N"
     by (subst return_sets_cong[where N=N]) (simp_all add: bind_return')
 qed
 
@@ -458,7 +458,7 @@
   "rel_fun op = (rel_fun cr_pmf cr_pmf) (\<lambda>f M. distr M (count_space UNIV) f) map_pmf"
 proof -
   have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
-     (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
+     (\<lambda>f M. M \<bind> (return (count_space UNIV) o f)) map_pmf"
     unfolding map_pmf_def[abs_def] comp_def by transfer_prover
   then show ?thesis
     by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
@@ -584,7 +584,7 @@
 
 lemma bind_pair_pmf:
   assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
-  shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
+  shows "measure_pmf (pair_pmf A B) \<bind> M = (measure_pmf A \<bind> (\<lambda>x. measure_pmf B \<bind> (\<lambda>y. M (x, y))))"
     (is "?L = ?R")
 proof (rule measure_eqI)
   have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -316,7 +316,7 @@
 
 primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
-| "C n (Suc m) \<omega> = C n m \<omega> \<guillemotright>= eP (n + m)"
+| "C n (Suc m) \<omega> = C n m \<omega> \<bind> eP (n + m)"
 
 lemma measurable_C[measurable]:
   "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
@@ -338,7 +338,7 @@
 qed (auto intro!: prob_space_return simp: space_PiM)
 
 lemma split_C:
-  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<guillemotright>= C (n + m) l) = C n (m + l) \<omega>"
+  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>"
 proof (induction l)
   case 0
   with \<omega> show ?case