src/HOL/Hyperreal/NSA.thy
changeset 20562 c2f672be8522
parent 20554 c433e78d4203
child 20563 44eda2314aab
--- a/src/HOL/Hyperreal/NSA.thy	Sun Sep 17 16:44:05 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Sun Sep 17 16:44:51 2006 +0200
@@ -357,7 +357,8 @@
 lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
 by (simp add: HFinite_def)
 
-lemma HFinite_hnorm_iff [iff]: "(hnorm x \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_hnorm_iff [iff]:
+  "(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
 by (simp add: HFinite_def)
 
 lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"