doc-src/TutorialI/Protocol/Public.thy

--- a/doc-src/TutorialI/Protocol/Public.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -22,14 +22,19 @@
 abbreviation priK :: "agent \<Rightarrow> key"
 where "priK x  \<equiv>  invKey(pubK x)"
 (*<*)
-primrec
+overloading initState \<equiv> initState
+begin
+
+primrec initState where
         (*Agents know their private key and all public keys*)
   initState_Server:  "initState Server     =    
                          insert (Key (priK Server)) (Key ` range pubK)"
-  initState_Friend:  "initState (Friend i) =    
+| initState_Friend:  "initState (Friend i) =    
                          insert (Key (priK (Friend i))) (Key ` range pubK)"
-  initState_Spy:     "initState Spy        =    
+| initState_Spy:     "initState Spy        =    
                          (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+
+end
 (*>*)
 
 text {*