fixed possibility_tac;
authorwenzelm
Fri, 20 Mar 2009 17:04:44 +0100
changeset 30608d9805c5b5d2e
parent 30607 c3d1590debd8
child 30609 983e8b6e4e69
fixed possibility_tac;
doc-src/TutorialI/Protocol/Public.thy
     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