diff -r 23a8c5ac35f8 -r 69916a850301 doc-src/TutorialI/Protocol/Public.thy
--- 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 {*