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:17:10 +0100
changeset 2574 3a832a3c6376
parent 2573 f3e04805895a
child 2575 65abf447151b
Correction to Problem 24
src/FOL/ex/cla.ML file | annotate | diff | comparison | revisions
src/FOLP/ex/cla.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/ex/cla.ML	Fri Jan 31 17:15:55 1997 +0100
+++ b/src/FOL/ex/cla.ML	Fri Jan 31 17:17:10 1997 +0100
@@ -207,7 +207,7 @@
 
 writeln"Problem 24";
 goal FOL.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)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (Fast_tac 1); 
 result();
--- a/src/FOLP/ex/cla.ML	Fri Jan 31 17:15:55 1997 +0100
+++ b/src/FOLP/ex/cla.ML	Fri Jan 31 17:17:10 1997 +0100
@@ -192,7 +192,7 @@
 
 writeln"Problem 24";
 goal FOLP.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)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (fast_tac FOLP_cs 1); 
 result();
isabelle