src/HOL/Auth/Event.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  text{*The constant "spies" is retained for compatibility's sake*}
     1.5  
     1.6  abbreviation (input)
     1.7 -  spies  :: "event list => msg set"
     1.8 +  spies  :: "event list => msg set" where
     1.9    "spies == knows Spy"
    1.10  
    1.11  text{*Spy has access to his own key for spoof messages, but Server is secure*}