# HG changeset patch
# User haftmann
# Date 1424016082 -3600
# Node ID ded0ff7540373f04443bae52f7b2396742197351
# Parent  6e685f9c9aa5dc9c95016c5035d5411ccced2f55
dropped unused rules

diff -r 6e685f9c9aa5 -r ded0ff754037 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -113,7 +113,6 @@
   "x * (y + z) = (x * y) + (x * z)"
   "x ^ (Suc q) = x * (x ^ q)"
   "x ^ (2*n) = (x ^ n) * (x ^ n)"
-  "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
   by (simp_all add: algebra_simps power_add power2_eq_square
     power_mult_distrib power_mult del: one_add_one)
 
diff -r 6e685f9c9aa5 -r ded0ff754037 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
@@ -166,7 +166,7 @@
 
       val _ =
         check_ops semiringN sr_ops 5 andalso
-        check_rules semiringN sr_rules 37 andalso
+        check_rules semiringN sr_rules 36 andalso
         check_ops ringN r_ops 2 andalso
         check_rules ringN r_rules 2 andalso
         check_ops fieldN f_ops 2 andalso
@@ -261,7 +261,7 @@
      pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
      pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
      pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
-     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38, _, _] = sr_rules;
+     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38, _] = sr_rules;
 
 val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
 val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;