# HG changeset patch
# User paulson
# Date 854727355 -3600
# Node ID f3e04805895a4387a1a20c4f7a575c6c26a670be
# Parent  8a47f85e7a03055d2911dd3854c61273e20ea298
Correction to Problem 24 (with unsatisfactory proof)

diff -r 8a47f85e7a03 -r f3e04805895a src/FOL/ex/int.ML
--- a/src/FOL/ex/int.ML	Fri Jan 31 17:13:19 1997 +0100
+++ b/src/FOL/ex/int.ML	Fri Jan 31 17:15:55 1997 +0100
@@ -260,7 +260,7 @@
 
 writeln"Problem 21";
 goal IFOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))";
-(*NOT PROVED*)
+(*NOT PROVED; needs quantifier duplication*)
 
 writeln"Problem 22";
 goal IFOL.thy "(ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
@@ -274,8 +274,12 @@
 
 writeln"Problem 24";
 goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
-\   --> (EX x. P(x)&R(x))";
+\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
+\   --> ~~(EX x. P(x)&R(x))";
+(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
+by Int.safe_tac; 
+by (etac impE 1);
+by (Int.fast_tac 1); 
 by (Int.fast_tac 1); 
 result();
 
diff -r 8a47f85e7a03 -r f3e04805895a src/FOLP/ex/int.ML
--- a/src/FOLP/ex/int.ML	Fri Jan 31 17:13:19 1997 +0100
+++ b/src/FOLP/ex/int.ML	Fri Jan 31 17:15:55 1997 +0100
@@ -264,8 +264,12 @@
 
 writeln"Problem 24";
 goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
-\   --> (EX x. P(x)&R(x))";
+\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
+\   --> ~~(EX x. P(x)&R(x))";
+(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
+by Int.safe_tac; 
+by (etac impE 1);
+by (Int.fast_tac 1); 
 by (Int.fast_tac 1); 
 result();