# HG changeset patch
# User huffman
# Date 1166128427 -3600
# Node ID 030f46b8c4b5cce3c8bab0d360dfbc8234e47316
# Parent  bf253f7075b481b26d68c153863b71f3900407fc
prove hyperpow_realpow using transfer

diff -r bf253f7075b4 -r 030f46b8c4b5 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 14 21:03:39 2006 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 14 21:33:47 2006 +0100
@@ -202,7 +202,7 @@
 
 lemma hyperpow_realpow:
       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-by (simp add: star_of_def hypnat_of_nat_eq hyperpow)
+by transfer (rule refl)
 
 lemma hyperpow_SReal [simp]:
      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"