--- a/Flask.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Flask.thy	Thu May 30 09:15:19 2013 +0800
@@ -434,15 +434,19 @@
 | "procs_of_shm (Attach p h flag # \<tau>) = 
     (procs_of_shm \<tau>) (h := insert (p, flag) (procs_of_shm \<tau> h))"
 | "procs_of_shm (Detach p h # \<tau>) =
-    (procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+    (procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
 | "procs_of_shm (DeleteShM p h # \<tau>) = (procs_of_shm \<tau>) (h := {})"
 | "procs_of_shm (Clone p p' fds shms # \<tau>) = 
     (\<lambda> h. if (h \<in> shms) 
-          then (procs_of_shm \<tau> h) \<union> {(p', flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h}
+          then (procs_of_shm \<tau> h) \<union> {(p', flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h}
           else procs_of_shm \<tau> h)"
 | "procs_of_shm (Execve p f fds # \<tau>) = 
-    (\<lambda> h. procs_of_shm \<tau> h - {(p, flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
-| "procs_of_shm (e # \<tau>)          = procs_of_shm \<tau>"
+    (\<lambda> h. procs_of_shm \<tau> h - {(p, flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+| "procs_of_shm (Kill p p' # s) = 
+    (\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (Exit p # s) = 
+    (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
 
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
@@ -765,6 +769,7 @@
 
 
 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+where
   "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
 
 end