equal
deleted
inserted
replaced
177 by (simp add: numeral_1_eq_1) |
177 by (simp add: numeral_1_eq_1) |
178 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False |
178 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False |
179 if_True add_0 add_Suc add_number_of_left mult_number_of_left |
179 if_True add_0 add_Suc add_number_of_left mult_number_of_left |
180 numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 |
180 numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1 |
181 numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1 |
181 numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1 |
182 iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min |
182 iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min |
183 iszero_number_of_Pls iszero_0 not_iszero_Numeral1 |
183 iszero_number_of_Pls iszero_0 not_iszero_Numeral1 |
184 |
184 |
185 lemmas semiring_norm = comp_arith |
185 lemmas semiring_norm = comp_arith |
186 |
186 |
187 ML {* |
187 ML {* |