changeset 90 | 5c7a69cef18b |
parent 23 | 2c7fedb2713c |
child 98 | f353b187526a |
--- a/ex/cla.ML Fri Jun 24 15:11:39 1994 +0200 +++ b/ex/cla.ML Wed Jun 29 12:04:04 1994 +0200 @@ -336,8 +336,8 @@ writeln"Problem 43 NOT PROVED AUTOMATICALLY"; goal HOL.thy - "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = p(z,y)::bool)) \ -\ --> (! x. (! y. q(x,y) = q(y,x)::bool))"; + "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \ +\ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))"; writeln"Problem 44";