diff -r 2a3cc8e1723a -r f2024fed9f0c src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Public.thy	Tue Feb 13 13:16:27 2001 +0100
@@ -8,30 +8,39 @@
 Private and public keys; initial states of agents
 *)
 
-Public = Event + 
+theory Public = Event
+files ("Public_lemmas.ML"):
 
 consts
-  pubK    :: agent => key
+  pubK    :: "agent => key"
 
 syntax
-  priK    :: agent => key
+  priK    :: "agent => key"
 
 translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
   "priK x"  == "invKey(pubK x)"
 
 primrec
         (*Agents know their private key and all public keys*)
-  initState_Server  "initState Server     =    
+  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)"
 
 
-rules
+axioms
   (*Public keys are disjoint, and never clash with private keys*)
-  inj_pubK        "inj pubK"
-  priK_neq_pubK   "priK A ~= pubK B"
+  inj_pubK:        "inj pubK"
+  priK_neq_pubK:   "priK A ~= pubK B"
+
+use "Public_lemmas.ML"
+
+(*Specialized methods*)
+
+method_setup possibility = {*
+    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+    "for proving possibility theorems"
 
 end