src/HOL/Groebner_Basis.thy
changeset 26086 3c243098b64a
parent 25250 b3a485b98963
child 26199 04817a8802f2
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sat Feb 16 16:52:09 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Feb 17 06:49:53 2008 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4    if_True add_0 add_Suc add_number_of_left mult_number_of_left
     1.5    numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
     1.6    numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
     1.7 -  iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
     1.8 +  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
     1.9    iszero_number_of_Pls iszero_0 not_iszero_Numeral1
    1.10  
    1.11  lemmas semiring_norm = comp_arith