# HG changeset patch
# User huffman
# Date 1228426209 28800
# Node ID 1ff53ff7041dc4eef7bb26dd87afc830c0506e84
# Parent  af325cd29b1545fb8ef6fc2ac5a87c5fa7bda90e
include iszero_simps in lemmas comp_arith

diff -r af325cd29b15 -r 1ff53ff7041d src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Dec 04 12:32:38 2008 -0800
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 04 13:30:09 2008 -0800
@@ -173,12 +173,12 @@
 
 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
   by (simp add: numeral_1_eq_1)
+
 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
   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_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
-  iszero_number_of_Pls iszero_0 not_iszero_Numeral1
+  numeral_0_eq_0[symmetric] numerals[symmetric]
+  iszero_simps not_iszero_Numeral1
 
 lemmas semiring_norm = comp_arith