Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Correction to Problem 24
authorpaulson
Fri, 31 Jan 1997 17:50:47 +0100
changeset 2575 65abf447151b
parent 2574 3a832a3c6376
child 2576 390c9fb786b5
Correction to Problem 24
src/HOL/ex/cla.ML file | annotate | diff | comparison | revisions
src/HOL/ex/mesontest.ML file | annotate | diff | comparison | revisions 
--- 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();
--- 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();
isabelle