equal
deleted
inserted
replaced
197 apply safe |
197 apply safe |
198 apply (drule spec, erule exE) |
198 apply (drule spec, erule exE) |
199 apply (drule spec, erule impE) |
199 apply (drule spec, erule impE) |
200 apply (erule BufAC_Asm_antiton [THEN antitonPD]) |
200 apply (erule BufAC_Asm_antiton [THEN antitonPD]) |
201 apply (erule is_ub_thelub) |
201 apply (erule is_ub_thelub) |
202 apply (tactic "smp_tac @{context} 3 1") |
202 apply (tactic "smp_tac \<^context> 3 1") |
203 apply (drule is_ub_thelub) |
203 apply (drule is_ub_thelub) |
204 apply (drule (1) mp) |
204 apply (drule (1) mp) |
205 apply (drule (1) mp) |
205 apply (drule (1) mp) |
206 apply (erule mp) |
206 apply (erule mp) |
207 apply (drule BufAC_Cmt_iterate_all [THEN iffD1]) |
207 apply (drule BufAC_Cmt_iterate_all [THEN iffD1]) |