# HG changeset patch
# User huffman
# Date 1178727921 -7200
# Node ID ff6559234a8938c6eb84017fb0732671d34cedc2
# Parent  2a3e9c7b894c1bc6816fffc32836b9ecbc1a774f
add lemma of_hypreal_hyperpow

diff -r 2a3e9c7b894c -r ff6559234a89 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed May 09 07:53:08 2007 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed May 09 18:25:21 2007 +0200
@@ -562,4 +562,9 @@
 lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
 by transfer (rule refl)
 
+lemma of_hypreal_hyperpow:
+  "\<And>x n. of_hypreal (x pow n) =
+   (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n"
+by transfer (rule of_real_power)
+
 end