equal
deleted
inserted
replaced
173 \ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ |
173 \ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ |
174 \ Says B A (Nonce NB) : set evs \ |
174 \ Says B A (Nonce NB) : set evs \ |
175 \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; |
175 \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; |
176 by (parts_induct_tac 1); |
176 by (parts_induct_tac 1); |
177 by (Fake_parts_insert_tac 1); |
177 by (Fake_parts_insert_tac 1); |
178 by (Step_tac 1); |
178 by Safe_tac; |
179 by (blast_tac (!claset addSEs partsEs) 1); |
179 by (blast_tac (!claset addSEs partsEs) 1); |
180 **) |
180 **) |