--- a/src/HOL/Hyperreal/NSA.thy Wed May 09 18:25:21 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed May 09 18:25:44 2007 +0200
@@ -103,6 +103,11 @@
"\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y"
by transfer (rule norm_mult)
+lemma hnorm_hyperpow:
+ "\<And>(x::'a::{real_normed_div_algebra,recpower} star) n.
+ hnorm (x pow n) = hnorm x pow n"
+by transfer (rule norm_power)
+
lemma hnorm_one [simp]:
"hnorm (1\<Colon>'a::real_normed_div_algebra star) = 1"
by transfer (rule norm_one)