--- a/Flask.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Flask.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -473,10 +473,17 @@
     (\<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>"
 
+inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
+| "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk>
+   \<Longrightarrow> info_flow_shm s p p''"
+(*
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
   "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. 
     (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
+*)
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
 where