| changeset 5453 | 30cb9d280014 |
| parent 5434 | 9b4bed3f394c |
| child 5480 | 93c21fee39f8 |
--- a/src/HOL/Auth/NS_Shared.ML Thu Sep 10 17:23:51 1998 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Thu Sep 10 17:25:13 1998 +0200 @@ -252,7 +252,7 @@ by (assume_tac 2); by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS Crypt_Spy_analz_bad]) 1); -by (blast_tac (claset() addDs [unique_session_keys]) 1); +by (blast_tac (claset() addSDs [unique_session_keys]) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE);