# HG changeset patch
# User paulson
# Date 880710752 -3600
# Node ID 9bfac4684f2f8362a5a77eeb1d8beb431070741f
# Parent  561242f8606b92db2b6630febb8249badf39826f
New example

diff -r 561242f8606b -r 9bfac4684f2f src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Nov 28 10:52:04 1997 +0100
+++ b/src/HOL/ex/set.ML	Fri Nov 28 10:52:32 1997 +0100
@@ -17,6 +17,11 @@
 by (blast_tac (claset() delrules [UNIV_I]) 1);
 result();
 
+(*variant of the benchmark above*)
+goal Set.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+by (blast_tac (claset() delrules [UNIV_I]) 1);
+(*just Blast_tac takes 27 seconds instead of 2.2*)
+result();
 
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)