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.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")