# HG changeset patch
# User huffman
# Date 1313450293 25200
# Node ID 5cdad94bdc2906772b1cacc7662e1ef8480cb08a
# Parent  903bfe95fecea2edab7ca17b1c607b2510eaa2ef
remove extraneous subsection heading

diff -r 903bfe95fece -r 5cdad94bdc29 src/HOL/Lim.thy
--- 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"