changeset 30510 | 4120fc59dd85 |
parent 27882 | eaa9fef9f4c1 |
child 30549 | d2d7874648bd |
--- a/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 19:58:26 2009 +0100 @@ -11,7 +11,7 @@ method_setup safety = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} "for proving safety properties" method_setup ensures_tac = {*