added a new example due to Robin Arthan

--- 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";