diff -r 093ea91498e6 -r 47500d0881f9 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Apr 09 09:37:48 2014 +0200
+++ b/src/HOL/Power.thy	Wed Apr 09 09:37:49 2014 +0200
@@ -661,7 +661,7 @@
   "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   by (simp add: divide_inverse) (rule power_inverse)
 
-lemma power_divide [field_simps]:
+lemma power_divide [field_simps, divide_simps]:
   "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
 apply (cases "b = 0")
 apply (simp add: power_0_left)