diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy
index b468cabd9f..c974e9edd8 100644
--- a/lib/Monads/trace/Trace_Empty_Fail.thy
+++ b/lib/Monads/trace/Trace_Empty_Fail.thy
@@ -21,8 +21,9 @@ definition empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" where
   "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> Failed \<in> snd ` (m s)"
 
 text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close>
-\<comment> \<open>definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where
-  "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"\<close>
+definition mk_ef ::
+  "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set" where
+  "mk_ef S \<equiv> if mres S = {} then S \<union> {([], Failed)} else S"
 
 
 subsection \<open>WPC setup\<close>
@@ -66,7 +67,7 @@ subsection \<open>Wellformed monads\<close>
 
 (*
   Collect generic empty_fail lemmas here:
-   - naming convention is emtpy_fail_NAME.
+   - naming convention is empty_fail_NAME.
    - add lemmas with assumptions to [empty_fail_cond] set
    - add lemmas without assumption to [empty_fail_term] set
 *)
@@ -195,9 +196,9 @@ lemma empty_fail_assert_opt[empty_fail_term]:
   "empty_fail (assert_opt x)"
   by (simp add: assert_opt_def empty_fail_term split: option.splits)
 
-\<comment> \<open>lemma empty_fail_mk_ef[empty_fail_term]:
+lemma empty_fail_mk_ef[empty_fail_term]:
   "empty_fail (mk_ef o m)"
-  by (simp add: empty_fail_def mk_ef_def)\<close>
+  by (simp add: empty_fail_def mk_ef_def)
 
 lemma empty_fail_gets_the[empty_fail_term]:
   "empty_fail (gets_the f)"
diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy
index e287245d49..7ddffb245c 100644
--- a/lib/Monads/trace/Trace_Monad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -727,16 +727,16 @@ section "Combinators that have conditions with side effects"
 definition notM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
   "notM m = do c \<leftarrow> m; return (\<not> c) od"
 
-definition
-  whileM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
+definition whileM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
   "whileM C B \<equiv> do
     c \<leftarrow> C;
     whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c;
     return ()
   od"
 
-definition
-  ifM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow>
+definition ifM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow>
           ('s, 'a) tmonad" where
   "ifM test t f = do
     c \<leftarrow> test;
@@ -751,12 +751,12 @@ definition ifME ::
     if c then t else f
    odE"
 
-definition
-  whenM :: "('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
+definition whenM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
   "whenM t m = ifM t m (return ())"
 
-definition
-  orM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
+definition orM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
   "orM a b = ifM a (return True) b"
 
 definition
diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy
index 20587e6cb8..2e0815222d 100644
--- a/lib/Monads/trace/Trace_Monad_Equations.thy
+++ b/lib/Monads/trace/Trace_Monad_Equations.thy
@@ -47,7 +47,7 @@ lemma throwError_bind:
 
 lemma bind_bindE_assoc:
   "((f >>= g) >>=E h)
-    = f >>= (\<lambda>rv. g rv >>=E h)"
+   = f >>= (\<lambda>rv. g rv >>=E h)"
   by (simp add: bindE_def bind_assoc)
 
 lemma returnOk_bind:
@@ -67,7 +67,7 @@ lemma cart_singleton_image:
 
 lemma liftE_bindE_handle:
   "((liftE f >>=E (\<lambda>x. g x)) <handle> h)
-      = f >>= (\<lambda>x. g x <handle> h)"
+   = f >>= (\<lambda>x. g x <handle> h)"
   by (simp add: liftE_bindE handleE_def handleE'_def
                 bind_assoc)
 
@@ -89,7 +89,7 @@ lemma liftE_bindE_assoc:
 
 lemma unlessE_throw_catch_If:
   "catch (unlessE P (throwError e) >>=E f) g
-      = (if P then catch (f ()) g else g e)"
+   = (if P then catch (f ()) g else g e)"
   by (simp add: unlessE_def catch_throwError split: if_split)
 
 lemma whenE_bindE_throwError_to_if:
@@ -125,13 +125,13 @@ lemma all_rv_choice_fn_eq_pred:
 
 lemma all_rv_choice_fn_eq:
   "\<lbrakk> \<And>rv. \<exists>fn. f rv = g fn \<rbrakk>
-    \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
+   \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
   using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\<top>]
   by (simp add: fun_eq_iff)
 
 lemma gets_the_eq_bind:
   "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
-     \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
+   \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
   apply (clarsimp dest!: all_rv_choice_fn_eq)
   apply (rule_tac x="\<lambda>s. case (fn s) of None \<Rightarrow> None | Some v \<Rightarrow> fna v s" in exI)
   apply (simp add: gets_the_def bind_assoc exec_gets
@@ -141,7 +141,7 @@ lemma gets_the_eq_bind:
 
 lemma gets_the_eq_bindE:
   "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
-     \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
+   \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
   apply (simp add: bindE_def)
   apply (erule gets_the_eq_bind)
   apply (simp add: lift_def gets_the_returns split: sum.split)
@@ -167,9 +167,9 @@ lemma ex_const_function:
 
 lemma gets_the_condsE:
   "(\<exists>fn. whenE P f = gets_the (fn o fn'))
-            = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
+   = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
   "(\<exists>fn. unlessE P g = gets_the (fn o fn'))
-            = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))"
+   = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))"
   by (simp add: whenE_def unlessE_def gets_the_returns ex_const_function
          split: if_split)+
 
@@ -183,7 +183,7 @@ lemma liftME_return:
 
 lemma fold_bindE_into_list_case:
   "(doE v \<leftarrow> f; case_list (g v) (h v) x odE)
-      = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)"
+   = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)"
   by (simp split: list.split)
 
 lemma whenE_liftE:
@@ -230,10 +230,9 @@ lemma modify_id_return:
  "modify id = return ()"
   by (simp add: simpler_modify_def return_def)
 
-
 lemma liftE_bind_return_bindE_returnOk:
   "liftE (v >>= (\<lambda>rv. return (f rv)))
-     = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))"
+   = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))"
   by (simp add: liftE_bindE, simp add: liftE_def returnOk_def)
 
 lemma bind_eqI:
@@ -241,12 +240,12 @@ lemma bind_eqI:
 
 lemma unlessE_throwError_returnOk:
   "(if P then returnOk v else throwError x)
-    = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))"
+   = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))"
   by (cases P, simp_all add: unlessE_def)
 
 lemma gets_the_bind_eq:
   "\<lbrakk> f s = Some x; g x s = h s \<rbrakk>
-    \<Longrightarrow> (gets_the f >>= g) s = h s"
+   \<Longrightarrow> (gets_the f >>= g) s = h s"
   by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def)
 
 lemma zipWithM_x_modify:
@@ -261,7 +260,7 @@ lemma zipWithM_x_modify:
 
 lemma assert2:
   "(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od)
-     = (do v \<leftarrow> assert (P \<and> Q); c od)"
+   = (do v \<leftarrow> assert (P \<and> Q); c od)"
   by (simp add: assert_def split: if_split)
 
 lemma assert_opt_def2:
@@ -270,20 +269,20 @@ lemma assert_opt_def2:
 
 lemma gets_assert:
   "(do v1 \<leftarrow> assert v; v2 \<leftarrow> gets f; c v1 v2 od)
-     = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)"
+   = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)"
   by (simp add: simpler_gets_def return_def assert_def fail_def bind_def
          split: if_split)
 
 lemma modify_assert:
   "(do v2 \<leftarrow> modify f; v1 \<leftarrow> assert v; c v1 od)
-    = (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)"
+   = (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)"
   by (simp add: simpler_modify_def return_def assert_def fail_def bind_def
          split: if_split)
 
 lemma gets_fold_into_modify:
   "do x \<leftarrow> gets f; modify (g x) od = modify (\<lambda>s. g (f s) s)"
   "do x \<leftarrow> gets f; _ \<leftarrow> modify (g x); h od
-     = do modify (\<lambda>s. g (f s) s); h od"
+   = do modify (\<lambda>s. g (f s) s); h od"
   by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
                     exec_get exec_put)
 
diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy
index ffc3879ad2..80f4ab5f7a 100644
--- a/lib/Monads/trace/Trace_More_VCG.thy
+++ b/lib/Monads/trace/Trace_More_VCG.thy
@@ -16,7 +16,7 @@ begin
 
 lemma hoare_take_disjunct:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace>
-    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>"
   by (erule hoare_strengthen_post, simp)
 
 lemma hoare_post_add:
@@ -94,12 +94,12 @@ lemmas hoare_lift_Pf_pre_conj' = hoare_lift_Pf2_pre_conj[where Q=P and P=P for P
 
 lemma hoare_if_r_and:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
-  = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>"
+   = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_convert_imp:
-  "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow>
-    \<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>"
+  "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>"
   apply (simp only: imp_conv_disj)
   apply (erule(1) hoare_vcg_disj_lift)
   done
@@ -112,8 +112,8 @@ lemma hoare_vcg_ex_lift_R:
   done
 
 lemma hoare_case_option_wpR:
-  "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk> \<Longrightarrow>
-  \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-"
+  "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk>
+   \<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-"
   by (cases v) auto
 
 lemma hoare_vcg_conj_liftE_R:
@@ -214,9 +214,10 @@ lemma list_cases_weak_wp:
   assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>"
   shows
   "\<lbrace>P_A and P_B\<rbrace>
-    case ts of
-      [] \<Rightarrow> a
-    | x#xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>"
+   case ts of
+       [] \<Rightarrow> a
+     | x#xs \<Rightarrow> b x xs
+   \<lbrace>Q\<rbrace>"
   apply (cases ts)
   apply (simp, rule hoare_weaken_pre, rule assms, simp)+
   done
@@ -225,18 +226,18 @@ lemmas hoare_FalseE_R = hoare_FalseE[where E="\<top>\<top>", folded validE_R_def
 
 lemma hoare_vcg_if_lift2:
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>"
 
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
   by (auto simp: valid_def split_def)
 
 lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"
 
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
   by (auto simp: valid_def validE_R_def validE_def split_def)
 
 lemma hoare_vcg_imp_liftE:
@@ -294,7 +295,7 @@ lemma set_shrink_proof:
   assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
   shows
   "\<lbrace>\<lambda>s. \<forall>S'. S' \<subseteq> S s \<longrightarrow> P S'\<rbrace>
-     f
+   f
    \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
   apply (clarsimp simp: valid_def)
   apply (drule spec, erule mp)
@@ -378,7 +379,7 @@ lemma valid_return_unit:
 
 lemma hoare_weak_lift_imp_conj:
   "\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
-    \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"
+   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"
   apply (rule hoare_vcg_conj_lift)
    apply (rule hoare_weak_lift_imp)
    apply assumption+
@@ -403,9 +404,10 @@ lemma hoare_vcg_disj_lift_R:
 lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def]
 
 lemma valid_case_option_post_wp:
-  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>) \<Longrightarrow>
-    \<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace>
-       f \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>"
+  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace>
+   f
+   \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>"
   by (cases ep, simp_all add: hoare_vcg_prop)
 
 lemma P_bool_lift:
@@ -485,13 +487,13 @@ lemma hoare_ex_pre: (* safe, unlike hoare_vcg_ex_lift *)
   by (fastforce simp: valid_def)
 
 lemma hoare_ex_pre_conj:
-  "(\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>)
-  \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
+  "\<lbrakk>\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_conj_lift_inv:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>;
-   \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
+    \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
    \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>"
    by (fastforce simp: valid_def)
 
@@ -518,7 +520,7 @@ lemma validE_R_sp:
 
 lemma valid_set_take_helper:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace>
-    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>"
   apply (erule hoare_strengthen_post)
   apply (clarsimp dest!: in_set_takeD)
   done
@@ -556,7 +558,7 @@ lemma hoare_vcg_imp_lift_R:
 
 lemma hoare_disj_division:
   "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
-     \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
+   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
   apply safe
    apply (rule hoare_pre_imp)
     prefer 2
@@ -573,8 +575,8 @@ lemma hoare_grab_asm:
   by (cases G, simp+)
 
 lemma hoare_grab_asm2:
-  "(P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>)
-  \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>"
+  "\<lbrakk>P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_grab_exs:
@@ -589,8 +591,8 @@ lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s
   by (rule hoare_pre, wp, simp)
 
 lemma hoare_vcg_conj_lift_R:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk> \<Longrightarrow>
-     \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-"
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-"
   apply (simp add: validE_R_def validE_def)
   apply (drule(1) hoare_vcg_conj_lift)
   apply (erule hoare_strengthen_post)
@@ -640,7 +642,7 @@ lemma other_hoare_in_monad_post:
 
 lemma weak_if_wp:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
+   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
   by (auto simp add: valid_def split_def)
 
 lemma weak_if_wp':
@@ -666,7 +668,7 @@ lemma validE_R_abstract_rv:
 
 lemma validE_cases_valid:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
-      \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (simp add: validE_def)
   apply (erule hoare_strengthen_post)
   apply (simp split: sum.split_asm)
@@ -691,12 +693,10 @@ lemma hoare_gen_asm_conj:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
-
 lemma hoare_add_K:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I\<rbrace>"
   by (fastforce simp: valid_def)
 
-
 lemma valid_rv_lift:
   "\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>"
   by (fastforce simp: valid_def)
@@ -707,20 +707,19 @@ lemma valid_imp_ex:
 
 lemma valid_rv_split:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk>
-  \<Longrightarrow>
-  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_rv_split:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
-  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (clarsimp simp: valid_def)
   apply (case_tac a, fastforce+)
   done
 
-lemma combine_validE: "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>;
-         \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk> \<Longrightarrow>
-         \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>"
+lemma combine_validE:
+  "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
+   \<Longrightarrow> \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>"
   apply (clarsimp simp: validE_def valid_def split: sum.splits)
   apply (erule allE, erule (1) impE)+
   apply (drule (1) bspec)+
diff --git a/lib/Monads/trace/Trace_No_Throw.thy b/lib/Monads/trace/Trace_No_Throw.thy
index edaa66800b..f5174f1ecd 100644
--- a/lib/Monads/trace/Trace_No_Throw.thy
+++ b/lib/Monads/trace/Trace_No_Throw.thy
@@ -31,6 +31,8 @@ lemma no_throw_def':
   by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
 
 
+subsection \<open>no_throw rules\<close>
+
 lemma no_throw_returnOk[simp]:
   "no_throw P (returnOk a)"
   unfolding no_throw_def