--- a/src/HOL/Tools/semiring_normalizer.ML Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Sun Feb 15 17:01:22 2015 +0100
@@ -249,17 +249,12 @@
fun zerone_conv ctxt cv =
zero1_numeral_conv ctxt then_conv cv then_conv numeral01_conv ctxt;
-val natarith = [@{thm "numeral_plus_numeral"}, @{thm "diff_nat_numeral"},
- @{thm "numeral_times_numeral"}, @{thm "numeral_eq_iff"},
- @{thm "numeral_less_iff"}];
-val nat_add_ss =
- simpset_of
- (put_simpset HOL_basic_ss @{context}
- addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
- @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
- @{thm add_numeral_left}, @{thm Suc_eq_plus1}]
- @ map (fn th => th RS sym) @{thms numerals});
+val nat_add_ss = simpset_of
+ (put_simpset HOL_basic_ss @{context}
+ addsimps @{thms arith_simps} @ @{thms diff_nat_numeral} @ @{thms rel_simps}
+ @ @{thms if_False if_True Nat.add_0 add_Suc add_numeral_left Suc_eq_plus1}
+ @ map (fn th => th RS sym) @{thms numerals});
fun nat_add_conv ctxt =
zerone_conv ctxt (Simplifier.rewrite (put_simpset nat_add_ss ctxt));