doc-src/TutorialI/Protocol/Public.thy
changeset 30608 d9805c5b5d2e
parent 30607 c3d1590debd8
child 32149 ef59550a55d3
     1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 17:04:44 2009 +0100
     1.3 @@ -152,7 +152,7 @@
     1.4  
     1.5  (*Tactic for possibility theorems*)
     1.6  ML {*
     1.7 -fun possibility ctxt =
     1.8 +fun possibility_tac ctxt =
     1.9      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    1.10      (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
    1.11       THEN