--- a/src/HOL/Groebner_Basis.thy Wed May 05 16:46:19 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Wed May 05 16:53:21 2010 +0200
@@ -5,10 +5,10 @@
header {* Semiring normalization and Groebner Bases *}
theory Groebner_Basis
-imports Numeral_Simprocs
+imports Numeral_Simprocs Nat_Transfer
uses
"Tools/Groebner_Basis/normalizer_data.ML"
- ("Tools/Groebner_Basis/normalizer.ML")
+ "Tools/Groebner_Basis/normalizer.ML"
("Tools/Groebner_Basis/groebner.ML")
begin
@@ -16,7 +16,6 @@
setup NormalizerData.setup
-
locale gb_semiring =
fixes add mul pwr r0 r1
assumes add_a:"(add x (add y z) = add (add x y) z)"
--- a/src/HOL/Nat_Numeral.thy Wed May 05 16:46:19 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed May 05 16:53:21 2010 +0200
@@ -687,6 +687,13 @@
lemmas nat_number' =
nat_number_of_Bit0 nat_number_of_Bit1
+lemmas nat_arith =
+ add_nat_number_of
+ diff_nat_number_of
+ mult_nat_number_of
+ eq_nat_number_of
+ less_nat_number_of
+
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (fact Let_def)