src/HOL/Hyperreal/SEQ.thy

--- a/src/HOL/Hyperreal/SEQ.thy	Wed Sep 27 05:19:24 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Sep 27 05:39:29 2006 +0200
@@ -160,9 +160,6 @@
 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
 by transfer simp
 
-lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
-by transfer simp
-
 lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
 by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)