Addition of blast_tac benchmark

--- a/src/ZF/func.ML	Tue Apr 15 10:22:50 1997 +0200
+++ b/src/ZF/func.ML	Tue Apr 15 10:23:17 1997 +0200
@@ -310,6 +310,11 @@
 	(*by (Blast_tac 1);  takes too long...*)
 qed "function_Union";
 
+(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
+goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+by (Blast_tac 1);
+result();
+
 goalw ZF.thy [Pi_def]
     "!!S. [| ALL f:S. EX C D. f:C->D; \
 \            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \