src/HOL/Power.thy
changeset 56481 47500d0881f9
parent 56480 093ea91498e6
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Power.thy	Wed Apr 09 09:37:48 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Apr 09 09:37:49 2014 +0200
     1.3 @@ -661,7 +661,7 @@
     1.4    "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
     1.5    by (simp add: divide_inverse) (rule power_inverse)
     1.6  
     1.7 -lemma power_divide [field_simps]:
     1.8 +lemma power_divide [field_simps, divide_simps]:
     1.9    "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
    1.10  apply (cases "b = 0")
    1.11  apply (simp add: power_0_left)