remove extraneous subsection heading

--- a/src/HOL/Lim.thy	Mon Aug 15 15:11:55 2011 -0700
+++ b/src/HOL/Lim.thy	Mon Aug 15 16:18:13 2011 -0700
@@ -386,8 +386,6 @@
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
   using assms by (rule tendsto_power)
 
-subsubsection {* Derived theorems about @{term LIM} *}
-
 lemma LIM_inverse:
   fixes L :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"