--- a/sound_defs_prop.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/sound_defs_prop.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -137,8 +137,9 @@
 apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp)
 apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
 apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e)
-apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps dest:nodel_imp_exists[where obj = "Proc pa"]
            split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
 done
 
 lemma initp_intact_I_exec:
@@ -191,6 +192,7 @@
 apply (erule_tac x = p in allE, case_tac e)
 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
            split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
 done
 
 end