--- a/src/HOL/Groebner_Basis.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Feb 17 06:49:53 2008 +0100
@@ -179,7 +179,7 @@
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] not_iszero_1
- iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
+ iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
iszero_number_of_Pls iszero_0 not_iszero_Numeral1
lemmas semiring_norm = comp_arith