src/FOL/ex/cla.ML
changeset 492 7bc980c7585e
parent 428 49cc52442678
child 644 112cf8574cf1
--- 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)) & \