# HG changeset patch
# User paulson
# Date 854729447 -3600
# Node ID 65abf447151b9f16172b130965ad5f9354936bac
# Parent  3a832a3c6376daa785f596c3d1fa02e22813dd2d
Correction to Problem 24

diff -r 3a832a3c6376 -r 65abf447151b src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri Jan 31 17:17:10 1997 +0100
+++ b/src/HOL/ex/cla.ML	Fri Jan 31 17:50:47 1997 +0100
@@ -204,7 +204,7 @@
 
 writeln"Problem 24";
 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
-\    ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x))  \
+\    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
 \   --> (? x. P(x)&R(x))";
 by (Fast_tac 1); 
 result();
diff -r 3a832a3c6376 -r 65abf447151b src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Fri Jan 31 17:17:10 1997 +0100
+++ b/src/HOL/ex/mesontest.ML	Fri Jan 31 17:50:47 1997 +0100
@@ -307,7 +307,7 @@
 
 writeln"Problem 24";  (*The first goal clause is useless*)
 goal HOL.thy "~(? x. S x & Q x) & (! x. P x --> Q x | R x) &  \
-\    ~(? x.P x) --> (? x.Q x) & (! x. Q x | R x --> S x)  \
+\    (~(? x.P x) --> (? x.Q x)) & (! x. Q x | R x --> S x)  \
 \   --> (? x. P x & R x)";
 by (safe_meson_tac 1); 
 result();