equal
deleted
inserted
replaced
266 by (ALLGOALS |
266 by (ALLGOALS |
267 (asm_simp_tac |
267 (asm_simp_tac |
268 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
268 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
269 (*Base*) |
269 (*Base*) |
270 by (Blast_tac 1); |
270 by (Blast_tac 1); |
271 (*RA4, RA2, Fake*) |
271 (*Fake*) |
272 by (REPEAT (spy_analz_tac 1)); |
272 by (spy_analz_tac 1); |
273 val raw_analz_image_freshK = result(); |
273 val raw_analz_image_freshK = result(); |
274 qed_spec_mp "analz_image_freshK"; |
274 qed_spec_mp "analz_image_freshK"; |
275 |
275 |
276 |
276 |
277 (*Instance of the lemma with H replaced by (sees lost Spy evs): |
277 (*Instance of the lemma with H replaced by (sees lost Spy evs): |