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.
merged
authorpopescua
Tue, 28 May 2013 13:22:06 +0200
changeset 52200 6324f30e23b6
parent 52199 d25fc4c0ff62 (current diff)
parent 52198 849cf98e03c3 (diff)
child 52201 9fcceb3c85ae
child 52203 055c392e79cf
merged
--- a/src/HOL/NSA/Filter.thy	Tue May 28 13:19:51 2013 +0200
+++ b/src/HOL/NSA/Filter.thy	Tue May 28 13:22:06 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