# HG changeset patch
# User huffman
# Date 1158504291 -7200
# Node ID c2f672be85224013eb6c0747f05f449ea66cc6a0
# Parent  6a6d8004322fde9b2d3490ffed0fc671c6200918
add type constraint to otherwise looping iff rule

diff -r 6a6d8004322f -r c2f672be8522 src/HOL/Hyperreal/NSA.thy
--- 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"