doc-src/TutorialI/Protocol/Public.thy
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