diff -r 5f462dfaf130 -r 5c7a69cef18b 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();