src/HOL/NSA/HLim.thy

--- a/src/HOL/NSA/HLim.thy	Tue Nov 27 19:43:00 2012 +0100
+++ b/src/HOL/NSA/HLim.thy	Tue Nov 27 20:01:57 2012 +0100
@@ -133,7 +133,7 @@
 lemma NSLIM_self: "(%x. x) -- a --NS> a"
 by (simp add: NSLIM_def)
 
-subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
+subsubsection {* Equivalence of @{term filter_lim} and @{term NSLIM} *}
 
 lemma LIM_NSLIM:
   assumes f: "f -- a --> L" shows "f -- a --NS> L"