src/HOL/Groebner_Basis.thy
changeset 36699 816da1023508
parent 36698 45f1a487cd27
child 36700 9b85b9d74b83
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:19 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed May 05 16:53:21 2010 +0200
     1.3 @@ -5,10 +5,10 @@
     1.4  header {* Semiring normalization and Groebner Bases *}
     1.5  
     1.6  theory Groebner_Basis
     1.7 -imports Numeral_Simprocs
     1.8 +imports Numeral_Simprocs Nat_Transfer
     1.9  uses
    1.10    "Tools/Groebner_Basis/normalizer_data.ML"
    1.11 -  ("Tools/Groebner_Basis/normalizer.ML")
    1.12 +  "Tools/Groebner_Basis/normalizer.ML"
    1.13    ("Tools/Groebner_Basis/groebner.ML")
    1.14  begin
    1.15  
    1.16 @@ -16,7 +16,6 @@
    1.17  
    1.18  setup NormalizerData.setup
    1.19  
    1.20 -
    1.21  locale gb_semiring =
    1.22    fixes add mul pwr r0 r1
    1.23    assumes add_a:"(add x (add y z) = add (add x y) z)"