author | wenzelm |
Fri, 20 Mar 2009 17:04:44 +0100 | |
changeset 30608 | d9805c5b5d2e |
parent 30607 | c3d1590debd8 |
child 30609 | 983e8b6e4e69 |
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