diff --git a/lib/Monads/nondet/Nondet_Monad.thy b/lib/Monads/nondet/Nondet_Monad.thy
index 2b86dce5df..e14cf17fd2 100644
--- a/lib/Monads/nondet/Nondet_Monad.thy
+++ b/lib/Monads/nondet/Nondet_Monad.thy
@@ -71,15 +71,15 @@ text \<open>
   operation may have failed, if @{text f} may have failed or @{text g} may
   have failed on any of the results of @{text f}.\<close>
 definition bind ::
-  "('s, 'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) nondet_monad) \<Rightarrow> ('s, 'b) nondet_monad"
-  (infixl ">>=" 60) where
+  "('s, 'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) nondet_monad) \<Rightarrow> ('s, 'b) nondet_monad" (infixl ">>=" 60)
+  where
   "bind f g \<equiv> \<lambda>s. (\<Union>(fst ` case_prod g ` fst (f s)),
                    True \<in> snd ` case_prod g ` fst (f s) \<or> snd (f s))"
 
 text \<open>Sometimes it is convenient to write @{text bind} in reverse order.\<close>
 abbreviation (input) bind_rev ::
-  "('c \<Rightarrow> ('a, 'b) nondet_monad) \<Rightarrow> ('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad"
-  (infixl "=<<" 60) where
+  "('c \<Rightarrow> ('a, 'b) nondet_monad) \<Rightarrow> ('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad" (infixl "=<<" 60)
+  where
   "g =<< f \<equiv> f >>= g"
 
 text \<open>
@@ -106,8 +106,8 @@ definition select :: "'a set \<Rightarrow> ('s,'a) nondet_monad" where
   "select A \<equiv> \<lambda>s. (A \<times> {s}, False)"
 
 definition alternative ::
-  "('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad"
-  (infixl "\<sqinter>" 20) where
+  "('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad" (infixl "\<sqinter>" 20)
+  where
   "f \<sqinter> g \<equiv> \<lambda>s. (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s))"
 
 text \<open>
@@ -559,8 +559,8 @@ text \<open>
   if the left-hand side throws no exception:\<close>
 definition handle_elseE ::
   "('s, 'e + 'a) nondet_monad \<Rightarrow> ('e \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow>
-   ('a \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> ('s, 'ee + 'b) nondet_monad"
-  ("_ <handle> _ <else> _" 10) where
+   ('a \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> ('s, 'ee + 'b) nondet_monad" ("_ <handle> _ <else> _" 10)
+  where
   "f <handle> handler <else> continue \<equiv>
    do v \<leftarrow> f;
       case v of Inl e  \<Rightarrow> handler e
diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy
index c2eaa42beb..f0d093b77e 100644
--- a/lib/Monads/trace/Trace_Monad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -135,8 +135,9 @@ text \<open>
 definition select :: "'a set \<Rightarrow> ('s, 'a) tmonad" where
   "select A \<equiv> \<lambda>s. (Pair [] ` Result ` (A \<times> {s}))"
 
-definition alternative :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad"
-  (infixl "\<sqinter>" 20) where
+definition alternative ::
+  "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad" (infixl "\<sqinter>" 20)
+  where
   "f \<sqinter> g \<equiv> \<lambda>s. (f s \<union> g s)"
 
 text \<open>
@@ -315,8 +316,8 @@ text \<open>
   the right-hand side is skipped if the left-hand side
   produced an exception.\<close>
 definition bindE ::
-  "('s, 'e + 'a) tmonad \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> ('s, 'e + 'b) tmonad"
-  (infixl ">>=E" 60) where
+  "('s, 'e + 'a) tmonad \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> ('s, 'e + 'b) tmonad" (infixl ">>=E" 60)
+  where
   "f >>=E g \<equiv> f >>= lift g"
 
 text \<open>
@@ -652,8 +653,8 @@ text \<open>
   practice: the exception handle (potentially) throws exception
   of the same type as the left-hand side.\<close>
 definition handleE ::
-  "('s, 'x + 'a) tmonad \<Rightarrow> ('x \<Rightarrow> ('s, 'x + 'a) tmonad) \<Rightarrow> ('s, 'x + 'a) tmonad"
-  (infix "<handle>" 10) where
+  "('s, 'x + 'a) tmonad \<Rightarrow> ('x \<Rightarrow> ('s, 'x + 'a) tmonad) \<Rightarrow> ('s, 'x + 'a) tmonad" (infix "<handle>" 10)
+  where
   "handleE \<equiv> handleE'"
 
 text \<open>
@@ -661,8 +662,8 @@ text \<open>
   if the left-hand side throws no exception:\<close>
 definition handle_elseE ::
   "('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow> ('a \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow>
-   ('s, 'ee + 'b) tmonad"
-  ("_ <handle> _ <else> _" 10) where
+   ('s, 'ee + 'b) tmonad" ("_ <handle> _ <else> _" 10)
+  where
   "f <handle> handler <else> continue \<equiv>
    do v \<leftarrow> f;
    case v of Inl e  \<Rightarrow> handler e