--- a/ex/cla.ML Thu Jul 21 10:52:00 1994 +0200
+++ b/ex/cla.ML Wed Jul 27 19:08:40 1994 +0200
@@ -163,6 +163,10 @@
by (best_tac HOL_dup_cs 1);
result();
+goal HOL.thy "? x. (? y. P(y)) --> P(x)";
+by (best_tac HOL_dup_cs 1);
+result();
+
writeln"Hard examples with quantifiers";
writeln"Problem 18";