# HG changeset patch
# User lcp
# Date 775328894 -7200
# Node ID 7bc980c7585e15dbd569ebee591b680c13747d2d
# Parent  1a7717eca14566cd4f46d47ed860ffc20709fc65
added a new example due to Robin Arthan

diff -r 1a7717eca145 -r 7bc980c7585e src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Wed Jul 27 19:04:21 1994 +0200
+++ b/src/FOL/ex/cla.ML	Wed Jul 27 19:08:14 1994 +0200
@@ -162,6 +162,10 @@
 by (best_tac FOL_dup_cs 1);
 result();
 
+goal FOL.thy "EX x. (EX y. P(y)) --> P(x)";
+by (best_tac FOL_dup_cs 1);
+result();
+
 (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*)
 goal FOL.thy "EX x x'. ALL y. EX z z'. \
 \               (~P(y,y) | P(x,x) | ~S(z,x)) & \