--- a/src/HOL/Power.thy Tue Nov 17 12:01:19 2015 +0100 +++ b/src/HOL/Power.thy Tue Nov 17 12:32:08 2015 +0000 @@ -391,8 +391,6 @@ "(a / b) ^ n = a ^ n / b ^ n" by (induct n) simp_all -declare power_divide [where b = "numeral w" for w, simp] - end