src/HOL/Groebner_Basis.thy
changeset 23312 6e32a5bfc30f
parent 23266 50f0a4f12ed3
child 23327 1654013ec97c
equal deleted inserted replaced
23311:b1eb911bf22f 23312:6e32a5bfc30f
     9 imports NatBin
     9 imports NatBin
    10 uses
    10 uses
    11   "Tools/Groebner_Basis/misc.ML"
    11   "Tools/Groebner_Basis/misc.ML"
    12   "Tools/Groebner_Basis/normalizer_data.ML"
    12   "Tools/Groebner_Basis/normalizer_data.ML"
    13   ("Tools/Groebner_Basis/normalizer.ML")
    13   ("Tools/Groebner_Basis/normalizer.ML")
       
    14   ("Tools/Groebner_Basis/groebner.ML")
    14 begin
    15 begin
    15 
    16 
    16 subsection {* Semiring normalization *}
    17 subsection {* Semiring normalization *}
    17 
    18 
    18 setup NormalizerData.setup
    19 setup NormalizerData.setup