src/HOL/Auth/Shared.thy
changeset 3519 ab0a9fbed4c0
parent 3512 9dcb4daa15e8
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/Shared.thy	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -19,9 +19,9 @@
     1.4  
     1.5  primrec initState agent
     1.6          (*Server knows all long-term keys; other agents know only their own*)
     1.7 -  initState_Server  "initState lost Server     = Key `` range shrK"
     1.8 -  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
     1.9 -  initState_Spy     "initState lost Spy        = Key``shrK``lost"
    1.10 +  initState_Server  "initState Server     = Key `` range shrK"
    1.11 +  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    1.12 +  initState_Spy     "initState Spy        = Key``shrK``lost"
    1.13  
    1.14  
    1.15  rules