| changeset 3730 | 6933d20f335f |
| parent 3683 | aafe719dff14 |
| child 4091 | 771b1f6422a8 |
--- a/src/HOL/Auth/WooLam.ML Mon Sep 29 11:46:33 1997 +0200 +++ b/src/HOL/Auth/WooLam.ML Mon Sep 29 11:47:01 1997 +0200 @@ -175,6 +175,6 @@ \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Step_tac 1); +by Safe_tac; by (blast_tac (!claset addSEs partsEs) 1); **)