diff --git a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
index b163bf17cb42f93c3227f2468a603b13e8b3368c..773c299c30472dd85e7565e3c6f05983d0d32a7c 100644
--- a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
+++ b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
@@ -547,8 +547,7 @@ next
                 exec_mbindFStop_success list.set_intros(1) list.set_intros(2) valid_bind_cong)
 qed
 
-
-
+text\<open>Symbolic execution rules for assertions.\<close>
 lemma assert_suffix_seq : 
               "\<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p xs iostep; assert\<^sub>S\<^sub>E (P)) 
                \<Longrightarrow> \<forall>\<sigma>. P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q)))