src/HOL/Auth/Shared.thy
changeset 2064 5a5e508e2a2b
parent 2032 1bbf1bdcaf56
child 2078 b198b3d46fb4
--- a/src/HOL/Auth/Shared.thy	Mon Oct 07 10:47:01 1996 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon Oct 07 10:55:51 1996 +0200
@@ -23,7 +23,7 @@
         (*Server knows all 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"
+  initState_Spy     "initState lost Spy        = Key``shrK``lost"
 
 
 datatype  (*Messages, and components of agent stores*)