Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prove hyperpow_realpow using transfer
authorhuffman
Thu, 14 Dec 2006 21:33:47 +0100
changeset 21851 030f46b8c4b5
parent 21850 bf253f7075b4
child 21852 7f2853bd54bf
prove hyperpow_realpow using transfer
src/HOL/Hyperreal/HyperPow.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle