src/HOL/Groebner_Basis.thy
changeset 31790 05c92381363c
parent 31068 f591144b0f17
child 33296 a3924d1069e5
     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4  lemmas comp_arith =
     1.5    Let_def arith_simps nat_arith rel_simps neg_simps if_False
     1.6    if_True add_0 add_Suc add_number_of_left mult_number_of_left
     1.7 -  numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
     1.8 +  numeral_1_eq_1[symmetric] Suc_eq_plus1
     1.9    numeral_0_eq_0[symmetric] numerals[symmetric]
    1.10    iszero_simps not_iszero_Numeral1
    1.11