src/HOL/Auth/Shared.thy
changeset 5183 89f162de39cf
parent 3683 aafe719dff14
child 10833 c0844a30ea4e
     1.1 --- a/src/HOL/Auth/Shared.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    isSym_keys "isSymKey K"	(*All keys are symmetric*)
     1.5    inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
     1.6  
     1.7 -primrec initState agent
     1.8 +primrec
     1.9          (*Server knows all long-term keys; other agents know only their own*)
    1.10    initState_Server  "initState Server     = Key `` range shrK"
    1.11    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"