src/HOL/Auth/NS_Shared.thy
changeset 11117 55358999077d
parent 11104 f2024fed9f0c
child 11150 67387142225e
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Feb 14 12:22:49 2001 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Feb 14 13:01:02 2001 +0100
     1.3 @@ -173,7 +173,7 @@
     1.4            \<or> X \<in> analz (spies evs)"
     1.5  apply (frule Says_imp_knows_Spy)
     1.6  (*mystery: why is this frule needed?*)
     1.7 -apply (blast dest: cert_A_form  analz.Inj)
     1.8 +apply (blast dest: cert_A_form analz.Inj)
     1.9  done
    1.10  
    1.11  (*Alternative version also provable
    1.12 @@ -224,8 +224,8 @@
    1.13  apply (erule ns_shared.induct, force)
    1.14  apply (frule_tac [7] Says_Server_message_form)
    1.15  apply (erule_tac [4] Says_S_message_form [THEN disjE])
    1.16 -apply (analz_freshK)
    1.17 -apply (spy_analz)
    1.18 +apply analz_freshK
    1.19 +apply spy_analz
    1.20  done
    1.21  
    1.22