changeset 30510 | 4120fc59dd85 |
parent 24123 | a0fc58900606 |
child 30549 | d2d7874648bd |
--- a/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 19:58:26 2009 +0100 @@ -372,7 +372,7 @@ method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} + SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} "for proving possibility theorems"