src/HOL/Power.thy
changeset 56480 093ea91498e6
parent 55811 aa1acc25126b
child 56481 47500d0881f9
     1.1 --- a/src/HOL/Power.thy	Wed Apr 09 09:37:47 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Apr 09 09:37:48 2014 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  context comm_monoid_mult
     1.5  begin
     1.6  
     1.7 -lemma power_mult_distrib:
     1.8 +lemma power_mult_distrib [field_simps]:
     1.9    "(a * b) ^ n = (a ^ n) * (b ^ n)"
    1.10    by (induct n) (simp_all add: mult_ac)
    1.11  
    1.12 @@ -661,7 +661,7 @@
    1.13    "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
    1.14    by (simp add: divide_inverse) (rule power_inverse)
    1.15  
    1.16 -lemma power_divide:
    1.17 +lemma power_divide [field_simps]:
    1.18    "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
    1.19  apply (cases "b = 0")
    1.20  apply (simp add: power_0_left)