# HG changeset patch
# User wenzelm
# Date 1354042917 -3600
# Node ID 3f0920f8a24eeb30ccb843424ffadb59abeed39f
# Parent  9a65279b5d27c8933675e815ca3371cab751b7d3
repaired text following 491c5c81c2e8;

diff -r 9a65279b5d27 -r 3f0920f8a24e 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"