# HG changeset patch
# User popescua
# Date 1369740126 -7200
# Node ID 6324f30e23b6bf69d2fb00748941535124fa241a
# Parent  d25fc4c0ff62df7eec2a040045f19b6f08217197# Parent  849cf98e03c36343e01dbae33d514729fce706d8
merged

diff -r d25fc4c0ff62 -r 6324f30e23b6 src/HOL/NSA/Filter.thy
--- 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."