changeset 30514 | e19d5b459a61 |
parent 26019 | ecbfe2645694 |
child 30548 | 2eef5e71edd6 |
1.1 --- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:10:46 2009 +0100 1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:53:09 2009 +0100 1.3 @@ -161,8 +161,7 @@ 1.4 resolve_tac [refl, conjI, @{thm Nonce_supply}])); 1.5 *} 1.6 1.7 -method_setup possibility = {* 1.8 - Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} 1.9 +method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *} 1.10 "for proving possibility theorems" 1.11 1.12 end