diff --git a/lib/Monads/trace/Trace_More_RG.thy b/lib/Monads/trace/Trace_More_RG.thy
index 0a5a8b5c4d..b409c3dffe 100644
--- a/lib/Monads/trace/Trace_More_RG.thy
+++ b/lib/Monads/trace/Trace_More_RG.thy
@@ -310,7 +310,7 @@ lemma ifM_throwError_returnOkI:
 lemmas state_unchanged_rg = in_inv_by_rgD [THEN sym]
 lemmas last_state_unchanged_rg = last_st_in_inv_by_rgD [THEN sym]
 
-\<comment> \<open>FIXME MC: name? move (both this one and validI in More_VCG)\<close>
+(*FIXME MC: name? move (both this one and validI in More_VCG)*)
 lemma validI_I:
   assumes px: "prefix_closed S"
   assumes gc: "\<And>s0 s tr res. \<lbrakk> P s0 s; (tr, res) \<in> (rely S R s0 s)\<rbrakk> \<Longrightarrow> guar_cond G s0 tr"
@@ -515,7 +515,7 @@ lemma rg_walk_assmsE:
    apply (auto simp: y split: sum.splits)
   done
 
-\<comment> \<open>FIXME MC: it is not immediately obvious what the validI equivalent of these rules should be, so I
+(*FIXME MC: it is not immediately obvious what the validI equivalent of these rules should be, so I
           think it is best to leave them until we have a specific use case.
 lemma univ_twp:
   "prefix_closed f \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<forall>(rv, s') \<in> mres (rely f R s0 s). Q rv s0 s'\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>"
@@ -548,7 +548,7 @@ lemma other_rg_in_monad_post:
   apply clarsimp
   apply (drule bspec, assumption, simp)
   done
-  qed\<close>
+  qed*)
 
 lemma weak_if_twp:
   "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index 3a5833a3ec..23d39732cd 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -289,12 +289,11 @@ lemma validIE_validE_no_trace_eq:
   apply (clarsimp simp: validI_valid_no_trace_eq)
   done
 
-\<comment> \<open>FIXME MC: name\<close>
+(*FIXME MC: name*)
 lemma validI_split:
   "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   by (auto simp: validI_def)
 
-\<comment> \<open>FIXME MC: name\<close>
 lemma validIE_split:
   "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   by (auto simp: validIE_def validI_split)
@@ -800,7 +799,7 @@ lemma validIE_eq_validI:
 
 subsection \<open>@{const liftM}\<close>
 
-\<comment> \<open>FIXME MC: make proof nicer\<close>
+(*FIXME: make proof nicer*)
 lemma rg_liftM_subst:
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> liftM f m \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>Q \<circ> f\<rbrace>"
   apply (clarsimp simp: validI_def)
@@ -1028,8 +1027,8 @@ lemma rg_vcg_const_imp_liftE_R:
   by (rule rg_strengthen_post)
      (fastforce intro!: rg_vcg_const_imp_lift split: sum.splits)+
 
-\<comment> \<open>FIXME MC: not clear whether we want these _T variants, and if we do whether they should be in the
-          wp set along with the above rules\<close>
+(*FIXME MC: not clear whether we want these _T variants, and if we do whether they should be in the
+          wp set along with the above rules*)
 lemmas rg_vcg_const_imp_lift_T = rg_vcg_const_imp_lift[where G="\<top>\<top>" and P''="\<top>\<top>", simplified]
 lemmas rg_vcg_const_imp_liftE_E_T = rg_vcg_const_imp_liftE_E[where G="\<top>\<top>" and P''="\<top>\<top>", simplified]
 lemmas rg_vcg_const_imp_liftE_R_T = rg_vcg_const_imp_liftE_R[where G="\<top>\<top>" and P''="\<top>\<top>", simplified]
@@ -1321,12 +1320,12 @@ lemma whenE_throwError_twp:
   "\<lbrace>\<lambda>s0 s. \<not>P \<longrightarrow> Q s0 s\<rbrace>,\<lbrace>R\<rbrace> whenE P (throwError e) \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,-"
   by (simp add: whenE_def returnOk_def throwError_def return_def validIE_def validI_def prefix_closed_def)
 
-\<comment> \<open>FIXME MC: not used, worth updating for validI or just delete?
+(*FIXME MC: not used, worth updating for validI or just delete?
 lemma select_throwError_twp:
   "\<lbrace>\<lambda>s0 s. \<forall>x\<in>S. Q x s0 s\<rbrace>,\<lbrace>R\<rbrace> select S >>= throwError \<lbrace>G\<rbrace>,-,\<lbrace>Q\<rbrace>"
-  by (simp add: bind_def throwError_def return_def select_def validIE_def validI_def prefix_closed_def)\<close>
+  by (simp add: bind_def throwError_def return_def select_def validIE_def validI_def prefix_closed_def)*)
 
-\<comment> \<open>FIXME MC: explore adding a rely_preserves definition for the first part of this precondition\<close>
+(*FIXME MC: explore adding a rely_preserves definition for the first part of this precondition*)
 lemma env_steps_twp[wp]:
   "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> env_steps \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   apply (simp add: env_steps_def)