# HG changeset patch # User lcp # Date 775328920 -7200 # Node ID f353b187526a6135e28ffff8ca89190f4b2547bc # Parent 3f4976d8c97f38c8a11f05cde90125ac42b83370 added a new example due to Robin Arthan diff -r 3f4976d8c97f -r f353b187526a ex/cla.ML --- 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";