equal
deleted
inserted
replaced
207 |
207 |
208 *) |
208 *) |
209 |
209 |
210 |
210 |
211 |
211 |
212 goal thy "!!ex .is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)"; |
212 goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"; |
213 by (case_tac "Finite ex" 1); |
213 by (case_tac "Finite ex" 1); |
214 by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1); |
214 by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1); |
215 ba 1; |
215 ba 1; |
216 be exE 1; |
216 be exE 1; |
217 br exec_prefix2closed 1; |
217 br exec_prefix2closed 1; |