--- a/src/HOL/Auth/NS_Public.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Public.thy Sat Aug 17 14:55:08 2002 +0200
@@ -103,8 +103,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
done
@@ -166,8 +165,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast intro: no_nonce_NS1_NS2)+
done