src/HOL/Power.thy
changeset 36349 39be26d1bc28
parent 35828 46cfc4b8112e
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Power.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -400,7 +400,7 @@
     1.4  
     1.5  text{*Perhaps these should be simprules.*}
     1.6  lemma power_inverse:
     1.7 -  fixes a :: "'a::{division_ring,division_by_zero,power}"
     1.8 +  fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
     1.9    shows "inverse (a ^ n) = (inverse a) ^ n"
    1.10  apply (cases "a = 0")
    1.11  apply (simp add: power_0_left)
    1.12 @@ -408,11 +408,11 @@
    1.13  done (* TODO: reorient or rename to inverse_power *)
    1.14  
    1.15  lemma power_one_over:
    1.16 -  "1 / (a::'a::{field,division_by_zero, power}) ^ n =  (1 / a) ^ n"
    1.17 +  "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n =  (1 / a) ^ n"
    1.18    by (simp add: divide_inverse) (rule power_inverse)
    1.19  
    1.20  lemma power_divide:
    1.21 -  "(a / b) ^ n = (a::'a::{field,division_by_zero}) ^ n / b ^ n"
    1.22 +  "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
    1.23  apply (cases "b = 0")
    1.24  apply (simp add: power_0_left)
    1.25  apply (rule nonzero_power_divide)