src/HOL/Lim.thy
changeset 44217 5cdad94bdc29
parent 44205 18da2a87421c
child 44218 f0e442e24816
     1.1 --- a/src/HOL/Lim.thy	Mon Aug 15 15:11:55 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Mon Aug 15 16:18:13 2011 -0700
     1.3 @@ -386,8 +386,6 @@
     1.4    shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
     1.5    using assms by (rule tendsto_power)
     1.6  
     1.7 -subsubsection {* Derived theorems about @{term LIM} *}
     1.8 -
     1.9  lemma LIM_inverse:
    1.10    fixes L :: "'a::real_normed_div_algebra"
    1.11    shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"