--- a/doc-src/TutorialI/Protocol/Public.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy Sat Oct 17 14:43:18 2009 +0200
@@ -25,11 +25,11 @@
primrec
(*Agents know their private key and all public keys*)
initState_Server: "initState Server =
- insert (Key (priK Server)) (Key ` range pubK)"
+ insert (Key (priK Server)) (Key ` range pubK)"
initState_Friend: "initState (Friend i) =
- insert (Key (priK (Friend i))) (Key ` range pubK)"
+ insert (Key (priK (Friend i))) (Key ` range pubK)"
initState_Spy: "initState Spy =
- (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+ (Key`invKey`pubK`bad) Un (Key ` range pubK)"
(*>*)
text {*