--- a/src/HOL/Auth/NS_Shared.thy Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Tue Apr 29 12:36:49 2003 +0200
@@ -302,9 +302,9 @@
apply (force dest!: Crypt_imp_keysFor)
txt{*NS3*}
apply blast
-txt{*NS4*}
-apply (blast dest!: B_trusts_NS3
- dest: Says_imp_knows_Spy [THEN analz.Inj]
+txt{*NS4*}
+apply (blast dest: B_trusts_NS3
+ Says_imp_knows_Spy [THEN analz.Inj]
Crypt_Spy_analz_bad unique_session_keys)
done
@@ -334,7 +334,7 @@
txt{*NS3*}
apply blast
txt{*NS4*}
-apply (blast dest!: B_trusts_NS3
+apply (blast dest: B_trusts_NS3
dest: Says_imp_knows_Spy [THEN analz.Inj]
unique_session_keys Crypt_Spy_analz_bad)
done