src/HOL/Auth/Event.thy
changeset 20768 1d478c2d621f
parent 18570 ffce25f9aa7f
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:32 2006 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:35 2006 +0200
     1.3 @@ -27,11 +27,10 @@
     1.4  
     1.5  
     1.6  text{*The constant "spies" is retained for compatibility's sake*}
     1.7 -syntax
     1.8 +
     1.9 +abbreviation (input)
    1.10    spies  :: "event list => msg set"
    1.11 -
    1.12 -translations
    1.13 -  "spies"   => "knows Spy"
    1.14 +  "spies == knows Spy"
    1.15  
    1.16  text{*Spy has access to his own key for spoof messages, but Server is secure*}
    1.17  specification (bad)