doc-src/TutorialI/Protocol/Public.thy

 
 (*Tactic for possibility theorems*)
 ML {*
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
+    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));
 *}