src/HOL/Auth/Yahalom2.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 4199 2b9fc1f08886
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -400,7 +400,7 @@
     1.4  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
     1.5  by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
     1.6  by (dtac B_trusts_YM4_shrK 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (rtac lemma 1);
    1.10  by (rtac Spy_not_see_encrypted_key 2);
    1.11  by (REPEAT_FIRST assume_tac);