src/HOL/Tools/res_axioms.ML
changeset 30510 4120fc59dd85
parent 30364 577edc39b501
child 30515 bca05b17b618
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4  
     1.5  val meson_method_setup = Method.add_methods
     1.6    [("meson", Method.thms_args (fn ths =>
     1.7 -      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
     1.8 +      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
     1.9      "MESON resolution proof procedure")];
    1.10  
    1.11  
    1.12 @@ -522,7 +522,7 @@
    1.13       end);
    1.14  
    1.15  val setup_methods = Method.add_methods
    1.16 -  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
    1.17 +  [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
    1.18      "conversion of goal to conjecture clauses")];
    1.19  
    1.20