src/HOL/Power.thy
 changeset 14438 6b41e98931f8 parent 14353 79f9fbef9106 child 14577 dbb95b825244
```     1.1 --- a/src/HOL/Power.thy	Fri Mar 05 15:26:04 2004 +0100
1.2 +++ b/src/HOL/Power.thy	Fri Mar 05 15:26:14 2004 +0100
1.3 @@ -171,13 +171,13 @@
1.4  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
1.5
1.6  lemma power_divide:
1.7 -    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
1.8 +    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
1.9  apply (case_tac "b=0", simp add: power_0_left)
1.10  apply (rule nonzero_power_divide)
1.11  apply assumption
1.12  done
1.13
1.14 -lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
1.15 +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
1.16  apply (induct_tac "n")
1.17  apply (auto simp add: power_Suc abs_mult)
1.18  done
1.19 @@ -301,8 +301,7 @@
1.20
1.21  instance nat :: ringpower
1.22  proof
1.23 -  fix z :: nat
1.24 -  fix n :: nat
1.25 +  fix z n :: nat
1.26    show "z^0 = 1" by simp
1.27    show "z^(Suc n) = z * (z^n)" by simp
1.28  qed
```