src/HOL/Auth/Event.thy

--- a/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -27,11 +27,10 @@
 
 
 text{*The constant "spies" is retained for compatibility's sake*}
-syntax
+
+abbreviation (input)
   spies  :: "event list => msg set"
-
-translations
-  "spies"   => "knows Spy"
+  "spies == knows Spy"
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}
 specification (bad)