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*)