--- 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.
--- 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 *}
--- 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
--- 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"