src/HOL/Auth/Shared.thy
changeset 3683 aafe719dff14
parent 3519 ab0a9fbed4c0
child 5183 89f162de39cf
     1.1 --- a/src/HOL/Auth/Shared.thy	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4          (*Server knows all long-term keys; other agents know only their own*)
     1.5    initState_Server  "initState Server     = Key `` range shrK"
     1.6    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
     1.7 -  initState_Spy     "initState Spy        = Key``shrK``lost"
     1.8 +  initState_Spy     "initState Spy        = Key``shrK``bad"
     1.9  
    1.10  
    1.11  rules