src/HOL/Auth/Event.thy

--- a/src/HOL/Auth/Event.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Event.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -29,7 +29,7 @@
 text{*The constant "spies" is retained for compatibility's sake*}
 
 abbreviation (input)
-  spies  :: "event list => msg set"
+  spies  :: "event list => msg set" where
   "spies == knows Spy"
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}