src/HOL/Auth/NS_Public.thy
changeset 13507 febb8e5d2a9d
parent 11366 b42287eb20cf
child 13922 75ae4244a596
     1.1 --- a/src/HOL/Auth/NS_Public.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -103,8 +103,7 @@
     1.4          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
     1.5         \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
     1.6  apply (erule rev_mp)   
     1.7 -apply (erule ns_public.induct, simp_all)
     1.8 -apply spy_analz
     1.9 +apply (erule ns_public.induct, simp_all, spy_analz)
    1.10  apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
    1.11  done
    1.12  
    1.13 @@ -166,8 +165,7 @@
    1.14         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
    1.15        \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    1.16  apply (erule rev_mp)
    1.17 -apply (erule ns_public.induct, simp_all)
    1.18 -apply spy_analz
    1.19 +apply (erule ns_public.induct, simp_all, spy_analz)
    1.20  apply (blast intro: no_nonce_NS1_NS2)+
    1.21  done
    1.22