src/HOL/Auth/Event.thy

--- a/src/HOL/Auth/Event.thy	Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/Event.thy	Wed Jan 04 16:13:53 2006 +0100
@@ -144,6 +144,8 @@
      Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
      parts.Body [THEN revcut_rl, standard]
 
+lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
+
 text{*Compatibility for the old "spies" function*}
 lemmas spies_partsEs = knows_Spy_partsEs
 lemmas Says_imp_spies = Says_imp_knows_Spy