1.1 --- a/src/ZF/ex/misc.ML	Mon Apr 21 10:16:01 1997 +0200
     1.2 +++ b/src/ZF/ex/misc.ML	Mon Apr 21 10:16:41 1997 +0200
     1.3 @@ -9,6 +9,11 @@
     1.4  
     1.5  writeln"ZF/ex/misc";
     1.6  
     1.7 +(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
     1.8 +goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
     1.9 +by (Blast_tac 1);
    1.10 +result();
    1.11 +
    1.12  set_current_thy"Perm";
    1.13  
    1.14  (*Example 12 (credited to Peter Andrews) from

     2.1 --- a/src/ZF/func.ML	Mon Apr 21 10:16:01 1997 +0200
     2.2 +++ b/src/ZF/func.ML	Mon Apr 21 10:16:41 1997 +0200
     2.3 @@ -310,11 +310,6 @@
     2.4  	(*by (Blast_tac 1);  takes too long...*)
     2.5  qed "function_Union";
     2.6  
     2.7 -(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
     2.8 -goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
     2.9 -by (Blast_tac 1);
    2.10 -result();
    2.11 -
    2.12  goalw ZF.thy [Pi_def]
    2.13      "!!S. [| ALL f:S. EX C D. f:C->D; \
    2.14  \            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \