# HG changeset patch
# User haftmann
# Date 1273161559 -7200
# Node ID ae84ddf03c58101b24a4083bc6dd626d7df8eab6
# Parent  4898bf6112091a13605b7fbbc1c3933b5cdb158b
dropped duplicate comp_arith

diff -r 4898bf611209 -r ae84ddf03c58 NEWS
--- a/NEWS	Thu May 06 17:55:12 2010 +0200
+++ b/NEWS	Thu May 06 17:59:19 2010 +0200
@@ -140,6 +140,8 @@
 
 *** HOL ***
 
+* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
+
 * Theory 'Finite_Set': various folding_* locales facilitate the application
 of the various fold combinators on finite sets.
 
diff -r 4898bf611209 -r ae84ddf03c58 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:55:12 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu May 06 17:59:19 2010 +0200
@@ -589,8 +589,6 @@
 end
 *}
 
-lemmas comp_arith = semiring_norm (*FIXME*)
-
 
 subsection {* Groebner Bases *}
 
diff -r 4898bf611209 -r ae84ddf03c58 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 17:55:12 2010 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 17:59:19 2010 +0200
@@ -11,7 +11,7 @@
 struct
 
 open Conv;
-val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
+val comp_ss = HOL_ss addsimps @{thms semiring_norm};
 
 fun strip_objimp ct =
   (case Thm.term_of ct of
diff -r 4898bf611209 -r ae84ddf03c58 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Thu May 06 17:55:12 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Thu May 06 17:59:19 2010 +0200
@@ -33,7 +33,7 @@
 
 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
   apply (simp only: power_Suc power_0)
-  apply (simp only: comp_arith)
+  apply (simp only: semiring_norm)
   oops
 
 lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"