# HG changeset patch
# User wenzelm
# Date 1369739671 -7200
# Node ID 849cf98e03c36343e01dbae33d514729fce706d8
# Parent  20071aef2a3b65fa393e67d9cde32713ac8be730
removed junk (cf. 667961fa6a60);

diff -r 20071aef2a3b -r 849cf98e03c3 src/HOL/NSA/Filter.thy
--- 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."