diff -r 6d3f7c7f70b0 -r 95f0d5243c85 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Thu Dec 05 18:07:27 1996 +0100
+++ b/src/HOL/Auth/Shared.thy	Thu Dec 05 18:56:18 1996 +0100
@@ -20,7 +20,7 @@
   initState :: [agent set, agent] => msg set
 
 primrec initState agent
-        (*Server knows all keys; other agents know only their own*)
+        (*Server knows all long-term keys; other agents know only their own*)
   initState_Server  "initState lost Server     = Key `` range shrK"
   initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
   initState_Spy     "initState lost Spy        = Key``shrK``lost"
@@ -40,13 +40,12 @@
   sees :: [agent set, agent, event list] => msg set
 
 primrec sees list
-        (*Initial knowledge includes all public keys and own private key*)
   sees_Nil  "sees lost A []       = initState lost A"
   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
-(*Agents generate "random" nonces.  Different traces always yield
-  different nonces.  Same applies for keys.*)
+(*Agents generate "random" nonces and keys.  These are uniquely determined by
+  the length of their argument, a trace.*)
 consts
   newN :: "event list => nat"
   newK :: "event list => key"