src/HOL/Auth/Shared.thy

 
 consts
   shrK    :: "agent => key"  (*symmetric keys*)
 
 axioms
-  isSym_keys: "K \\<in> symKeys"	(*All keys are symmetric*)
+  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
   inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
 
 primrec
         (*Server knows all long-term keys; other agents know only their own*)
   initState_Server:  "initState Server     = Key ` range shrK"

 
 use "Shared_lemmas.ML"
 
 (*Lets blast_tac perform this step without needing the simplifier*)
 lemma invKey_shrK_iff [iff]:
-     "(Key (invKey K) \\<in> X) = (Key K \\<in> X)"
+     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
 by auto;
 
 (*Specialized methods*)
 
 method_setup analz_freshK = {*

                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
                           ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
-    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts =>
+            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     "for proving possibility theorems"
 
 end