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