equal
deleted
inserted
replaced
181 apply (subgoal_tac "M ok G") |
181 apply (subgoal_tac "M ok G") |
182 prefer 2 apply (force intro: M_ok_iff [THEN iffD2]) |
182 prefer 2 apply (force intro: M_ok_iff [THEN iffD2]) |
183 apply (drule guaranteesD, assumption) |
183 apply (drule guaranteesD, assumption) |
184 apply (simp add: merge_spec_def merge_follows_def, blast) |
184 apply (simp add: merge_spec_def merge_follows_def, blast) |
185 apply (simp cong add: Follows_cong |
185 apply (simp cong add: Follows_cong |
186 add: refl_prefix |
186 add: refl_prefix |
187 mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def]) |
187 mono_bag_of [THEN subset_Follows_comp, THEN subsetD, |
|
188 unfolded metacomp_def]) |
188 done |
189 done |
189 |
190 |
190 end |
191 end |
191 |
192 |
192 |
193 |