equal
deleted
inserted
replaced
214 by (etac yahalom.induct 1); |
214 by (etac yahalom.induct 1); |
215 by analz_spies_tac; |
215 by analz_spies_tac; |
216 by (ALLGOALS |
216 by (ALLGOALS |
217 (asm_simp_tac |
217 (asm_simp_tac |
218 (simpset() addsimps expand_ifs |
218 (simpset() addsimps expand_ifs |
219 addsimps [analz_insert_eq, analz_insert_freshK] |
219 addsimps [analz_insert_eq, analz_insert_freshK]))); |
220 addsplits [expand_if]))); |
|
221 (*Oops*) |
220 (*Oops*) |
222 by (blast_tac (claset() addDs [unique_session_keys]) 3); |
221 by (blast_tac (claset() addDs [unique_session_keys]) 3); |
223 (*YM3*) |
222 (*YM3*) |
224 by (blast_tac (claset() delrules [impCE] |
223 by (blast_tac (claset() delrules [impCE] |
225 addSEs spies_partsEs |
224 addSEs spies_partsEs |