diff -r da4dd8b7ced4 -r 9dcb4daa15e8 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Jul 09 17:00:34 1997 +0200
+++ b/src/HOL/Auth/Shared.thy	Fri Jul 11 13:26:15 1997 +0200
@@ -5,10 +5,10 @@
 
 Theory of Shared Keys (common to all symmetric-key protocols)
 
-Server keys; initial states of agents; new nonces and keys; function "sees" 
+Shared, long-term keys; initial states of agents
 *)
 
-Shared = Message + List + Finite +
+Shared = Event + Finite +
 
 consts
   shrK    :: agent => key  (*symmetric keys*)
@@ -17,9 +17,6 @@
   isSym_keys "isSymKey K"	(*All keys are symmetric*)
   inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
 
-consts  (*Initial states of agents -- parameter of the construction*)
-  initState :: [agent set, agent] => msg set
-
 primrec initState agent
         (*Server knows all long-term keys; other agents know only their own*)
   initState_Server  "initState lost Server     = Key `` range shrK"
@@ -27,31 +24,6 @@
   initState_Spy     "initState lost Spy        = Key``shrK``lost"
 
 
-datatype  (*Messages, and components of agent stores*)
-  event = Says agent 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 {})"
-
-consts  
-  sees :: [agent set, agent, event list] => msg set
-
-primrec sees list
-  sees_Nil  "sees lost A []       = initState lost A"
-  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-
-
-constdefs
-  (*Set of items that might be visible to somebody: complement of the set
-        of fresh items*)
-  used :: event list => msg set
-    "used evs == parts (UN lost B. sees lost B evs)"
-
-
 rules
   (*Unlike the corresponding property of nonces, this cannot be proved.
     We have infinitely many agents and there is nothing to stop their