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.
removed junk (cf. 667961fa6a60);
authorwenzelm
Tue, 28 May 2013 13:14:31 +0200
changeset 52198 849cf98e03c3
parent 52197 20071aef2a3b
child 52200 6324f30e23b6
child 52210 0226035df99d
removed junk (cf. 667961fa6a60);
src/HOL/NSA/Filter.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/NSA/Filter.thy	Tue May 28 10:18:43 2013 +0200
+++ b/src/HOL/NSA/Filter.thy	Tue May 28 13:14:31 2013 +0200
@@ -264,7 +264,7 @@
 
 text "In this section we prove that superfrechet is closed
 with respect to unions of non-empty chains. We must show
-  1) Union of a chain is afind_theorems name: Union_chain_UNIV filter,
+  1) Union of a chain is a filter,
   2) Union of a chain contains frechet.
 
 Number 2 is trivial, but 1 requires us to prove all the filter rules."
isabelle