src/HOL/Groebner_Basis.thy
changeset 29230 155f6c110dfc
parent 29223 e09c53289830
parent 29039 8b9207f82a78
child 29233 ce6d35a0bed6
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Dec 12 20:03:30 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Dec 12 20:10:22 2008 +0100
     1.3 @@ -177,7 +177,8 @@
     1.4  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
     1.5    by (simp add: numeral_1_eq_1)
     1.6  
     1.7 -lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
     1.8 +lemmas comp_arith =
     1.9 +  Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.10    if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.11    numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
    1.12    numeral_0_eq_0[symmetric] numerals[symmetric]