Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/HyperPow.thy
changeset 21851 030f46b8c4b5
parent 21848 b35faf14a89f 
--- 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