src/HOL/Groebner_Basis.thy
changeset 28986 1ff53ff7041d
parent 28856 5e009a80fe6d
child 28987 dc0ab579a5ca
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Dec 04 12:32:38 2008 -0800
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Dec 04 13:30:09 2008 -0800
     1.3 @@ -173,12 +173,12 @@
     1.4  
     1.5  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
     1.6    by (simp add: numeral_1_eq_1)
     1.7 +
     1.8  lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
     1.9    if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.10    numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
    1.11 -  numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
    1.12 -  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
    1.13 -  iszero_number_of_Pls iszero_0 not_iszero_Numeral1
    1.14 +  numeral_0_eq_0[symmetric] numerals[symmetric]
    1.15 +  iszero_simps not_iszero_Numeral1
    1.16  
    1.17  lemmas semiring_norm = comp_arith
    1.18