# HG changeset patch
# User haftmann
# Date 1424016082 -3600
# Node ID 239bf09ee36f1dc0a6787469237b13342de874c6
# Parent  3850a2d20f19836e1b8d2ff5eede6b36dd528c2b
simpset with no redundancy

diff -r 3850a2d20f19 -r 239bf09ee36f src/HOL/Tools/semiring_normalizer.ML
--- 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));