--- a/src/HOL/Lim.thy Fri Feb 13 08:00:46 2009 +1100
+++ b/src/HOL/Lim.thy Thu Feb 12 20:36:41 2009 -0800
@@ -452,6 +452,11 @@
shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
by (rule LIM_inverse_fun [THEN LIM_compose])
+lemma LIM_sgn:
+ "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
+unfolding sgn_div_norm
+by (simp add: LIM_scaleR LIM_inverse LIM_norm)
+
subsection {* Continuity *}
@@ -529,6 +534,10 @@
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
+lemma isCont_sgn:
+ "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
+ unfolding isCont_def by (rule LIM_sgn)
+
lemma isCont_abs [simp]: "isCont abs (a::real)"
by (rule isCont_rabs [OF isCont_ident])