src/HOL/Power.thy
changeset 59867 58043346ca64
parent 59865 8a20dd967385
child 60155 91477b3a2d6b
     1.1 --- a/src/HOL/Power.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -705,7 +705,7 @@
     1.4  
     1.5  text{*Perhaps these should be simprules.*}
     1.6  lemma power_inverse:
     1.7 -  fixes a :: "'a::division_ring_inverse_zero"
     1.8 +  fixes a :: "'a::division_ring"
     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 @@ -713,11 +713,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_inverse_zero, power}) ^ n =  (1 / a) ^ n"
    1.17 +  "1 / (a::'a::{field, power}) ^ n =  (1 / a) ^ n"
    1.18    by (simp add: divide_inverse) (rule power_inverse)
    1.19  
    1.20  lemma power_divide [field_simps, divide_simps]:
    1.21 -  "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
    1.22 +  "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
    1.23  apply (cases "b = 0")
    1.24  apply (simp add: power_0_left)
    1.25  apply (rule nonzero_power_divide)