diff -r 5a1f81da3e12 -r a18a6dc14f76 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Fri Jul 26 12:18:50 1996 +0200
+++ b/src/HOL/Auth/Event.thy	Fri Jul 26 12:19:46 1996 +0200
@@ -26,7 +26,7 @@
 
 primrec initState agent
         (*Server knows all keys; other agents know only their own*)
-  initState_Server  "initState Server     = range (Key o serverKey)"
+  initState_Server  "initState Server     = Key `` range serverKey"
   initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
   initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
 
@@ -111,7 +111,7 @@
                    (serverKey A))) # evs : traces"
 
            (*We can't assume S=Server.  Agent A "remembers" her nonce.
-             May assume WLOG that she is NOT the Enemy, as the Fake rule.
+             May assume WLOG that she is NOT the Enemy: the Fake rule
              covers this case.  Can inductively show A ~= Server*)
     NS3  "[| evs: traces;  A ~= B;
              evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}