--- a/Delete_prop.thy	Thu Dec 05 20:13:30 2013 +0800
+++ b/Delete_prop.thy	Tue Dec 17 13:30:21 2013 +0800
@@ -229,6 +229,7 @@
   "no_del_event s \<Longrightarrow> \<not> deleted obj s"
 by (induct s, simp, case_tac a,auto)
 
+
 lemma nodel_exists_remains:
   "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"
 apply (drule_tac obj = obj in nodel_imp_un_deleted)