src/HOL/Groebner_Basis.thy
changeset 29039 8b9207f82a78
parent 28987 dc0ab579a5ca
child 29230 155f6c110dfc
--- a/src/HOL/Groebner_Basis.thy	Tue Dec 09 20:35:31 2008 -0800
+++ b/src/HOL/Groebner_Basis.thy	Tue Dec 09 20:36:20 2008 -0800
@@ -178,7 +178,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]