--- a/src/HOL/Power.thy Mon Apr 26 11:34:15 2010 +0200
+++ b/src/HOL/Power.thy Mon Apr 26 11:34:17 2010 +0200
@@ -400,7 +400,7 @@
text{*Perhaps these should be simprules.*}
lemma power_inverse:
- fixes a :: "'a::{division_ring,division_by_zero,power}"
+ fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
shows "inverse (a ^ n) = (inverse a) ^ n"
apply (cases "a = 0")
apply (simp add: power_0_left)
@@ -408,11 +408,11 @@
done (* TODO: reorient or rename to inverse_power *)
lemma power_one_over:
- "1 / (a::'a::{field,division_by_zero, power}) ^ n = (1 / a) ^ n"
+ "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n = (1 / a) ^ n"
by (simp add: divide_inverse) (rule power_inverse)
lemma power_divide:
- "(a / b) ^ n = (a::'a::{field,division_by_zero}) ^ n / b ^ n"
+ "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
apply (cases "b = 0")
apply (simp add: power_0_left)
apply (rule nonzero_power_divide)