diff -r f2569416d18b -r 414e04d7c2d6 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:21 1997 +0200
+++ b/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:27 1997 +0200
@@ -6,6 +6,9 @@
 Theory of events for security protocols
 
 Datatype of events; function "sees"; freshness
+
+"lost" agents have been broken by the Spy; their private keys and internal
+    stores are visible to him
 *)
 
 Event = Message + List + 
@@ -18,15 +21,7 @@
         | Notes agent       msg
 
 consts  
-  sees1 :: [agent, event] => msg set
-
-primrec sees1 event
-           (*Spy reads all traffic whether addressed to him or not*)
-  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
-  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
-
-consts  
-  lost :: agent set        (*agents whose private keys have been compromised*)
+  lost :: agent set        (*compromised agents*)
   sees :: [agent, event list] => msg set
 
 rules
@@ -34,6 +29,15 @@
   Spy_in_lost     "Spy: lost"
   Server_not_lost "Server ~: lost"
 
+consts  
+  sees1 :: [agent, event] => msg set
+
+primrec sees1 event
+           (*Spy reads all traffic whether addressed to him or not*)
+  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
+  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
+					 else {})"
+
 primrec sees list
   sees_Nil  "sees A []       = initState A"
   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"