src/HOL/Auth/Event.thy
changeset 32404 da3ca3c6ec81
parent 30549 d2d7874648bd
child 32960 69916a850301
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Aug 14 15:20:16 2009 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Aug 14 17:26:11 2009 +0100
     1.3 @@ -139,9 +139,11 @@
     1.4  
     1.5  text{*Elimination rules: derive contradictions from old Says events containing
     1.6    items known to be fresh*}
     1.7 +lemmas Says_imp_parts_knows_Spy = 
     1.8 +       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
     1.9 +
    1.10  lemmas knows_Spy_partsEs =
    1.11 -     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
    1.12 -     parts.Body [THEN revcut_rl, standard]
    1.13 +     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
    1.14  
    1.15  lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
    1.16