src/HOL/Auth/NS_Shared.thy
changeset 58860 fee7cfa69c50
parent 56681 e8d5d60d655e
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  apply (drule_tac [8] Says_Server_message_form)
     1.5  apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
     1.6  txt{*NS2, NS3*}
     1.7 -apply blast+; 
     1.8 +apply blast+ 
     1.9  done
    1.10  
    1.11  
    1.12 @@ -468,7 +468,7 @@
    1.13       Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
    1.14       Key K \<notin> analz (spies evs);
    1.15       A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
    1.16 - \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
    1.17 + \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
    1.18  apply (erule rev_mp)
    1.19  apply (erule rev_mp)
    1.20  apply (erule rev_mp)