Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
repaired text following 491c5c81c2e8;
authorwenzelm
Tue, 27 Nov 2012 20:01:57 +0100
changeset 50249 3f0920f8a24e
parent 50248 9a65279b5d27
child 50250 267bd685a69f
child 50256 ed9487289e04
repaired text following 491c5c81c2e8;
src/HOL/NSA/HLim.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle