--- a/Static.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Static.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -463,9 +463,16 @@
 where
   "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
 
+(*
 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
 where
   "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
+*)
+inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
+where
+  "info_flow_sshm sp sp"
+| "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
+   \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
 
 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"
 where