# HG changeset patch
# User haftmann
# Date 1273071201 -7200
# Node ID 816da1023508529729e1b450863236f29139ab6f
# Parent  45f1a487cd278c93b894b2007fd2e719e10d5ef4
moved nat_arith ot Nat_Numeral: clarified normalizer setup

diff -r 45f1a487cd27 -r 816da1023508 src/HOL/Groebner_Basis.thy
--- 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)"
diff -r 45f1a487cd27 -r 816da1023508 src/HOL/Nat_Numeral.thy
--- 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)