src/HOL/NSA/HLim.thy
changeset 50249 3f0920f8a24e
parent 41959 b460124855b8
child 50322 b06b95a5fda2
     1.1 --- a/src/HOL/NSA/HLim.thy	Tue Nov 27 19:43:00 2012 +0100
     1.2 +++ b/src/HOL/NSA/HLim.thy	Tue Nov 27 20:01:57 2012 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  lemma NSLIM_self: "(%x. x) -- a --NS> a"
     1.5  by (simp add: NSLIM_def)
     1.6  
     1.7 -subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
     1.8 +subsubsection {* Equivalence of @{term filter_lim} and @{term NSLIM} *}
     1.9  
    1.10  lemma LIM_NSLIM:
    1.11    assumes f: "f -- a --> L" shows "f -- a --NS> L"