equal
deleted
inserted
replaced
134 apply (rule conjI) |
134 apply (rule conjI) |
135 apply simp |
135 apply simp |
136 apply (blast dest: boundedD) |
136 apply (blast dest: boundedD) |
137 apply blast |
137 apply blast |
138 apply clarify |
138 apply clarify |
139 apply (rotate_tac -2) |
|
140 apply (erule allE) |
139 apply (erule allE) |
141 apply (erule impE) |
|
142 apply assumption |
|
143 apply (erule impE) |
140 apply (erule impE) |
144 apply assumption |
141 apply assumption |
145 apply (drule bspec) |
142 apply (drule bspec) |
146 apply assumption |
143 apply assumption |
147 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
144 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
433 apply (rule termination_lemma) |
430 apply (rule termination_lemma) |
434 apply assumption+ |
431 apply assumption+ |
435 defer |
432 defer |
436 apply assumption |
433 apply assumption |
437 apply clarsimp |
434 apply clarsimp |
438 apply (blast dest!: boundedD) |
|
439 done |
435 done |
440 |
436 |
441 |
437 |
442 lemma kildall_properties: includes semilat |
438 lemma kildall_properties: includes semilat |
443 shows "\<lbrakk> acc r; pres_type step n A; mono r step n A; |
439 shows "\<lbrakk> acc r; pres_type step n A; mono r step n A; |