src/HOL/Groebner_Basis.thy
changeset 47432 e1576d13e933
parent 47165 9344891b504b
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -43,8 +43,20 @@
     1.4  
     1.5  use "Tools/groebner.ML"
     1.6  
     1.7 -method_setup algebra = Groebner.algebra_method
     1.8 -  "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
     1.9 +method_setup algebra = {*
    1.10 +  let
    1.11 +    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.12 +    val addN = "add"
    1.13 +    val delN = "del"
    1.14 +    val any_keyword = keyword addN || keyword delN
    1.15 +    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.16 +  in
    1.17 +    Scan.optional (keyword addN |-- thms) [] --
    1.18 +     Scan.optional (keyword delN |-- thms) [] >>
    1.19 +    (fn (add_ths, del_ths) => fn ctxt =>
    1.20 +      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.21 +  end
    1.22 +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.23  
    1.24  declare dvd_def[algebra]
    1.25  declare dvd_eq_mod_eq_0[symmetric, algebra]