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