diff -r cc1e46225a81 -r 4ca824cd0c59 Static.thy --- a/Static.thy Thu May 30 15:28:57 2013 +0800 +++ b/Static.thy Mon Jun 03 10:34:58 2013 +0800 @@ -58,7 +58,7 @@ definition init_cph2spshs :: "t_process \ (t_sshm \ t_shm_attach_flag) set" where - "init_cph2spshs p \ {(sh, flag). \ h. (p, flag) \ init_procs_of_shm h \ + "init_cph2spshs p \ {(sh, flag)| sh flag h. (p, flag) \ init_procs_of_shm h \ init_ch2sshm h = Some sh}" definition init_cp2sproc :: "t_process \ t_sproc option" @@ -723,7 +723,7 @@ definition cph2spshs :: "t_state \ t_process \ t_sproc_sshm set" where - "cph2spshs s p \ {(sh, flag). \ h. (p, flag) \ procs_of_shm s h \ ch2sshm s h = Some sh}" + "cph2spshs s p \ {(sh, flag)| sh flag h. (p, flag) \ procs_of_shm s h \ ch2sshm s h = Some sh}" definition cp2sproc :: "t_state \ t_process \ t_sproc option" where