ex/mesontest.ML

--- a/ex/mesontest.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/mesontest.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -75,8 +75,8 @@
 
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\         --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 by (rtac ccontr 1);
 val [prem43] = gethyps 1;
 val nnf43 = make_nnf prem43;
@@ -161,7 +161,7 @@
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal HOL.thy "P=P::bool";
+goal HOL.thy "P=(P::bool)";
 by (safe_meson_tac 1);
 result();
 
@@ -404,8 +404,8 @@
 result();
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\         --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 by (safe_meson_tac 1);
 result();