changeset 4324 | 9bfac4684f2f |
parent 4153 | e534c4c32d54 |
child 4686 | 74a12e86b20b |
--- 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 ***)