src/HOL/Groebner_Basis.thy
changeset 30510 4120fc59dd85
parent 30242 aea5d7fa7ef5
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -253,7 +253,7 @@
     1.4  
     1.5  
     1.6  method_setup sring_norm = {*
     1.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
     1.8 +  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
     1.9  *} "semiring normalizer"
    1.10  
    1.11  
    1.12 @@ -431,7 +431,7 @@
    1.13      ((Scan.optional (keyword addN |-- thms) []) -- 
    1.14      (Scan.optional (keyword delN |-- thms) [])) src 
    1.15   #> (fn ((add_ths, del_ths), ctxt) => 
    1.16 -       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.17 +       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.18  end
    1.19  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.20  declare dvd_def[algebra]