Bu's Symbolic execution rules for assertions

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)))