equal
deleted
inserted
replaced
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') = |