# HG changeset patch
# User paulson
# Date 880709768 -3600
# Node ID 5f5df208b0e0ab6beccff4491a2eca0a6c09b613
# Parent  2a2956ccb86c8936b0a130a1b189caeee375b18f
New example

diff -r 2a2956ccb86c -r 5f5df208b0e0 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Fri Nov 28 07:41:24 1997 +0100
+++ b/src/ZF/ex/misc.ML	Fri Nov 28 10:36:08 1997 +0100
@@ -14,6 +14,11 @@
 by (Blast_tac 1);
 result();
 
+(*variant of the benchmark above*)
+goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+by (Blast_tac 1);
+result();
+
 context Perm.thy;
 
 (*Example 12 (credited to Peter Andrews) from