src/HOL/Auth/Event.thy
changeset 18570 ffce25f9aa7f
parent 17990 86d462f305e0
child 20768 1d478c2d621f
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Jan 04 10:28:31 2006 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Jan 04 16:13:53 2006 +0100
     1.3 @@ -144,6 +144,8 @@
     1.4       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
     1.5       parts.Body [THEN revcut_rl, standard]
     1.6  
     1.7 +lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
     1.8 +
     1.9  text{*Compatibility for the old "spies" function*}
    1.10  lemmas spies_partsEs = knows_Spy_partsEs
    1.11  lemmas Says_imp_spies = Says_imp_knows_Spy