equal
deleted
inserted
replaced
176 less_nat_number_of |
176 less_nat_number_of |
177 |
177 |
178 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)" |
178 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)" |
179 by (simp add: numeral_1_eq_1) |
179 by (simp add: numeral_1_eq_1) |
180 |
180 |
181 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False |
181 lemmas comp_arith = |
|
182 Let_def arith_simps nat_arith rel_simps neg_simps if_False |
182 if_True add_0 add_Suc add_number_of_left mult_number_of_left |
183 if_True add_0 add_Suc add_number_of_left mult_number_of_left |
183 numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 |
184 numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 |
184 numeral_0_eq_0[symmetric] numerals[symmetric] |
185 numeral_0_eq_0[symmetric] numerals[symmetric] |
185 iszero_simps not_iszero_Numeral1 |
186 iszero_simps not_iszero_Numeral1 |
186 |
187 |