equal
deleted
inserted
replaced
254 by (etac otway.induct 1); |
254 by (etac otway.induct 1); |
255 by analz_spies_tac; |
255 by analz_spies_tac; |
256 by (ALLGOALS |
256 by (ALLGOALS |
257 (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] |
257 (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] |
258 addsimps [analz_insert_eq, analz_insert_freshK] |
258 addsimps [analz_insert_eq, analz_insert_freshK] |
259 addsimps (pushes@expand_ifs)))); |
259 addsimps (pushes@split_ifs)))); |
260 (*Oops*) |
260 (*Oops*) |
261 by (blast_tac (claset() addSDs [unique_session_keys]) 4); |
261 by (blast_tac (claset() addSDs [unique_session_keys]) 4); |
262 (*OR4*) |
262 (*OR4*) |
263 by (Blast_tac 3); |
263 by (Blast_tac 3); |
264 (*OR3*) |
264 (*OR3*) |