diff -r 958cc116d03b -r e19d5b459a61 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:10:46 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:53:09 2009 +0100 @@ -161,8 +161,7 @@ resolve_tac [refl, conjI, @{thm Nonce_supply}])); *} -method_setup possibility = {* - Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} +method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *} "for proving possibility theorems" end