equal
deleted
inserted
replaced
178 by (simp add: numeral_1_eq_1) |
178 by (simp add: numeral_1_eq_1) |
179 |
179 |
180 lemmas comp_arith = |
180 lemmas comp_arith = |
181 Let_def arith_simps nat_arith rel_simps neg_simps if_False |
181 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 |
182 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 |
183 numeral_1_eq_1[symmetric] Suc_eq_plus1 |
184 numeral_0_eq_0[symmetric] numerals[symmetric] |
184 numeral_0_eq_0[symmetric] numerals[symmetric] |
185 iszero_simps not_iszero_Numeral1 |
185 iszero_simps not_iszero_Numeral1 |
186 |
186 |
187 lemmas semiring_norm = comp_arith |
187 lemmas semiring_norm = comp_arith |
188 |
188 |