squash lib/monads

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/nondet/Nondet_VCG.thy

@@ -32,15 +32,14 @@ text \<open>This section defines a Hoare logic for partial correctness for
   the empty set, the triple 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 Nondet_No_Fail).
-\<close>
+  calculus (see Nondet_No_Fail).\<close>
 definition valid ::
   "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> fst (f s). Q r s')"
 
 text \<open>
   We often reason about invariant predicates. The following provides shorthand syntax
-  that avoids repeating potentially long predicates. \<close>
+  that avoids repeating potentially long predicates.\<close>
 abbreviation (input) invariant ::
   "('s,'a) nondet_monad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) where
   "invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
@@ -60,7 +59,7 @@ lemma validE_def2:
 
 text \<open>
   The following two instantiations are convenient to separate reasoning for exceptional and
-  normal case. \<close>
+  normal case.\<close>
 (* Narrator: they are in fact not convenient, and are now considered a mistake that should have
              been an abbreviation instead. *)
 definition validE_R :: (* FIXME lib: this should be an abbreviation *)