lib/monads: fix remaining document preparation issues

Fix document preparation issues in the theory files that have been
added to ROOT in the previous commit.

Signed-off-by: Gerwin Klein <[email protected]>

lib/Monads/trace/Trace_Empty_Fail.thy

@@ -14,9 +14,9 @@ begin
 section \<open>Monads that are wellformed w.r.t. failure\<close>
 
 text \<open>
-  Usually, well-formed monads constructed from the primitives in Trace_Monad will have the following
-  property: if they return an empty set of completed results, there exists a trace corresponding to
-  a failed result.\<close>
+  Usually, well-formed monads constructed from the primitives in @{text Trace_Monad} will have the
+  following property: if they return an empty set of completed results, there exists a trace
+  corresponding to a failed result.\<close>
 definition empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" where
   "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> Failed \<in> snd ` (m s)"
 

lib/Monads/trace/Trace_Monad_Equations.thy

@@ -376,7 +376,7 @@ lemma select_empty_bind[simp]:
   by (simp add: select_def bind_def)
 
 
-subsection \<open>Alternative env_steps with repeat\<close>
+subsection \<open>Alternative @{text env_steps} with repeat\<close>
 
 lemma mapM_Cons:
   "mapM f (x # xs) = do

lib/Monads/trace/Trace_No_Fail.thy

@@ -144,7 +144,7 @@ lemma no_fail_assume_pre:
   "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
 
-\<comment> \<open>lemma no_fail_liftM_eq[simp]:
+\<^cancel>\<open>lemma no_fail_liftM_eq[simp]:
   "no_fail P (liftM f m) = no_fail P m"
   by (auto simp: liftM_def no_fail_def bind_def return_def)\<close>
 

lib/Monads/trace/Trace_No_Throw.thy

@@ -31,7 +31,7 @@ lemma no_throw_def':
   by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
 
 
-subsection \<open>no_throw rules\<close>
+subsection \<open>@{const no_throw} rules\<close>
 
 lemma no_throw_returnOk[simp]:
   "no_throw P (returnOk a)"

lib/Monads/trace/Trace_RG.thy

@@ -17,7 +17,7 @@ section \<open>Rely-Guarantee Logic\<close>
 subsection \<open>Validity\<close>
 
 text \<open>
-  This section defines a Rely_Guarantee logic for partial correctness for
+  This section defines a Rely-Guarantee logic for partial correctness for
   the interference trace monad.
 
   The logic is defined semantically. Rules work directly on the
@@ -36,7 +36,7 @@ text \<open>
   trace and no successful results then the quintuple is trivially valid. This
   means @{term "assert P"} does not require us to prove that @{term P} holds,
   but rather allows us to assume @{term P}! Proving non-failure is done via a
-  separate predicate and calculus (see Trace_No_Fail).\<close>
+  separate predicate and calculus (see @{text Trace_No_Fail}).\<close>
 
 primrec trace_steps :: "(tmid \<times> 's) list \<Rightarrow> 's \<Rightarrow> (tmid \<times> 's \<times> 's) set" where
     "trace_steps (elem # trace) s0 = {(fst elem, s0, snd elem)} \<union> trace_steps trace (snd elem)"
@@ -56,7 +56,7 @@ next
     done
 qed
 
-text \<open>rg_pred type: Rely-Guaranty predicates (state before => state after => bool)\<close>
+text \<open>@{text rg_pred} type: Rely-Guaranty predicates (@{text "state before => state after => bool"})\<close>
 type_synonym 's rg_pred = "'s \<Rightarrow> 's \<Rightarrow> bool"
 
 text \<open>Abbreviations for trivial postconditions (taking three arguments):\<close>

lib/Monads/trace/Trace_Total.thy

@@ -11,7 +11,7 @@ theory Trace_Total
   imports Trace_No_Fail
 begin
 
-section \<open>Total correctness for Trace_Monad and Trace_Monad with exceptions\<close>
+section \<open>Total correctness for @{text Trace_Monad} and @{text Trace_Monad} with exceptions\<close>
 
 subsection Definitions