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