diff -r 1a1df29d3507 -r d9dc04c3ea90 no_shm_selinux/S2ss_prop2.thy
--- a/no_shm_selinux/S2ss_prop2.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/S2ss_prop2.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -14,11 +14,11 @@
 apply (rule_tac x = obj in exI)
 thm co2sobj_other
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_bind:
@@ -27,11 +27,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_connect:
@@ -40,11 +40,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_listen:
@@ -53,11 +53,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_accept:
@@ -66,11 +66,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_send:
@@ -79,11 +79,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_recv:
@@ -92,11 +92,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_shutdown:
@@ -105,11 +105,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open