1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4  primrec
     1.5          (*Agents know their private key and all public keys*)
     1.6    initState_Server:  "initState Server     =    
     1.7 - 		         insert (Key (priK Server)) (Key ` range pubK)"
     1.8 +                         insert (Key (priK Server)) (Key ` range pubK)"
     1.9    initState_Friend:  "initState (Friend i) =    
    1.10 - 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
    1.11 +                         insert (Key (priK (Friend i))) (Key ` range pubK)"
    1.12    initState_Spy:     "initState Spy        =    
    1.13 - 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
    1.14 +                         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
    1.15  (*>*)
    1.16  
    1.17  text {*