equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Current_prop |
2 theory Current_prop |
3 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop |
3 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop |
4 begin |
4 begin |
5 (*>*) |
5 (*>*) |
6 |
|
7 ML {*quick_and_dirty := true*} |
|
8 |
6 |
9 context flask begin |
7 context flask begin |
10 |
8 |
11 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
9 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
12 apply (induct s arbitrary:p_flag) |
10 apply (induct s arbitrary:p_flag) |