ex/cla.ML
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";