| changeset 3000 | 7ecb8b6a3d7f |
| parent 2496 | 40efb87985b5 |
| child 4091 | 771b1f6422a8 |
--- a/src/ZF/ex/misc.ML Mon Apr 21 10:16:01 1997 +0200 +++ b/src/ZF/ex/misc.ML Mon Apr 21 10:16:41 1997 +0200 @@ -9,6 +9,11 @@ writeln"ZF/ex/misc"; +(*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(); + set_current_thy"Perm"; (*Example 12 (credited to Peter Andrews) from