src/FOL/ex/cla.ML
changeset 492 7bc980c7585e
parent 428 49cc52442678
child 644 112cf8574cf1
equal deleted inserted replaced
491:1a7717eca145 492:7bc980c7585e
   157 goal FOL.thy "EX x. P(x) --> P(a) & P(b)";
   157 goal FOL.thy "EX x. P(x) --> P(a) & P(b)";
   158 by (best_tac FOL_dup_cs 1);
   158 by (best_tac FOL_dup_cs 1);
   159 result();
   159 result();
   160 
   160 
   161 goal FOL.thy "EX z. P(z) --> (ALL x. P(x))";
   161 goal FOL.thy "EX z. P(z) --> (ALL x. P(x))";
       
   162 by (best_tac FOL_dup_cs 1);
       
   163 result();
       
   164 
       
   165 goal FOL.thy "EX x. (EX y. P(y)) --> P(x)";
   162 by (best_tac FOL_dup_cs 1);
   166 by (best_tac FOL_dup_cs 1);
   163 result();
   167 result();
   164 
   168 
   165 (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*)
   169 (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*)
   166 goal FOL.thy "EX x x'. ALL y. EX z z'. \
   170 goal FOL.thy "EX x x'. ALL y. EX z z'. \