--- a/src/HOL/Groebner_Basis.thy Fri Dec 12 20:03:30 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Dec 12 20:10:22 2008 +0100
@@ -177,7 +177,8 @@
lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
by (simp add: numeral_1_eq_1)
-lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
+lemmas comp_arith =
+ Let_def arith_simps nat_arith rel_simps neg_simps if_False
if_True add_0 add_Suc add_number_of_left mult_number_of_left
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
numeral_0_eq_0[symmetric] numerals[symmetric]