# HG changeset patch
# User wenzelm
# Date 1237565084 -3600
# Node ID d9805c5b5d2ef44ab6e4d4126bd80be322a5b11e
# Parent  c3d1590debd8df6937e5b62a5b2ddbd52cfe3d7b
fixed possibility_tac;

diff -r c3d1590debd8 -r d9805c5b5d2e 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