doc-src/TutorialI/Protocol/Public.thy

--- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 17:04:44 2009 +0100
@@ -152,7 +152,7 @@
 
 (*Tactic for possibility theorems*)
 ML {*
-fun possibility ctxt =
+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]))
      THEN