# HG changeset patch # User paulson # Date 1078496774 -3600 # Node ID 6b41e98931f8e97ba3bc755be37f67e0ccecc5f1 # Parent 92f6aa05b7bbbe6bcf96c0c1387e030adf776023 tweaks diff -r 92f6aa05b7bb -r 6b41e98931f8 src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Mar 05 15:26:04 2004 +0100 +++ b/src/HOL/Power.thy Fri Mar 05 15:26:14 2004 +0100 @@ -171,13 +171,13 @@ by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) lemma power_divide: - "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)" + "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)" apply (case_tac "b=0", simp add: power_0_left) apply (rule nonzero_power_divide) apply assumption done -lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n" +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n" apply (induct_tac "n") apply (auto simp add: power_Suc abs_mult) done @@ -301,8 +301,7 @@ instance nat :: ringpower proof - fix z :: nat - fix n :: nat + fix z n :: nat show "z^0 = 1" by simp show "z^(Suc n) = z * (z^n)" by simp qed