src/HOL/Auth/Shared.thy
changeset 2064 5a5e508e2a2b
parent 2032 1bbf1bdcaf56
child 2078 b198b3d46fb4
     1.1 --- a/src/HOL/Auth/Shared.thy	Mon Oct 07 10:47:01 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Mon Oct 07 10:55:51 1996 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4          (*Server knows all keys; other agents know only their own*)
     1.5    initState_Server  "initState lost Server     = Key `` range shrK"
     1.6    initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
     1.7 -  initState_Spy   "initState lost Spy      = Key``shrK``lost"
     1.8 +  initState_Spy     "initState lost Spy        = Key``shrK``lost"
     1.9  
    1.10  
    1.11  datatype  (*Messages, and components of agent stores*)