# 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