--- a/src/ZF/ex/misc.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/ex/misc.ML Mon Aug 17 13:09:08 1998 +0200
@@ -10,12 +10,12 @@
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}";
+Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
by (Blast_tac 1);
result();
(*variant of the benchmark above*)
-goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
by (Blast_tac 1);
result();