# HG changeset patch
# User huffman
# Date 1178661135 -7200
# Node ID 1ec078cca386cdef5bc5b265e6d1bd1c2cd59646
# Parent  ca2eb5eb615b07900dad0dfd7607751f8b78f505
add lemma Standard_hyperpow

diff -r ca2eb5eb615b -r 1ec078cca386 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 21:02:26 2007 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 23:52:15 2007 +0200
@@ -429,6 +429,10 @@
   hyperpow_def [transfer_unfold]:
   "R pow N = ( *f2* op ^) R N"
 
+lemma Standard_hyperpow [simp]:
+  "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
+unfolding hyperpow_def by simp
+
 lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
 by (simp add: hyperpow_def starfun2_star_n)
 
@@ -537,7 +541,7 @@
 
 lemma hyperpow_SReal [simp]:
      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
-by (simp add: hyperpow_def Reals_eq_Standard)
+by (simp add: Reals_eq_Standard)
 
 lemma hyperpow_zero_HNatInfinite [simp]:
      "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"