Static.thy
changeset 43 137358bd4921
parent 42 021672ec28f5
child 47 0960686df575
equal deleted inserted replaced
42:021672ec28f5 43:137358bd4921
   170   "is_many (S_proc sp   tag) = is_many_sproc sp"
   170   "is_many (S_proc sp   tag) = is_many_sproc sp"
   171 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
   171 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
   172 | "is_many (S_dir  sf      ) = is_many_sfile sf"
   172 | "is_many (S_dir  sf      ) = is_many_sfile sf"
   173 | "is_many (S_msgq sq      ) = is_many_smsgq sq"
   173 | "is_many (S_msgq sq      ) = is_many_smsgq sq"
   174 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
   174 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
   175 | "is_many _                 = False"
       
   176 
   175 
   177 (*
   176 (*
   178 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
   177 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
   179 where
   178 where
   180   "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = 
   179   "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') =