src/HOL/Word/Misc_Numeric.thy
changeset 44821 a92f65e174cf
parent 39910 10097e0a9dbd
child 44939 5930d35c976d
--- a/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -312,7 +312,7 @@
   apply safe
    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
    apply (drule le_iff_add [THEN iffD1])
-   apply (force simp: zpower_zadd_distrib)
+   apply (force simp: power_add)
   apply (rule mod_pos_pos_trivial)
    apply (simp)
   apply (rule power_strict_increasing)