--- a/src/HOL/ex/cla.ML Wed Apr 23 11:02:19 1997 +0200
+++ b/src/HOL/ex/cla.ML Wed Apr 23 11:05:18 1997 +0200
@@ -281,11 +281,10 @@
writeln"Problem 34 AMENDED (TWICE!!)";
(*Andrews's challenge*)
goal HOL.thy "((? x. ! y. p(x) = p(y)) = \
-\ ((? x. q(x)) = (! y. p(y)))) = \
-\ ((? x. ! y. q(x) = q(y)) = \
-\ ((? x. p(x)) = (! y. q(y))))";
+\ ((? x. q(x)) = (! y. p(y)))) = \
+\ ((? x. ! y. q(x) = q(y)) = \
+\ ((? x. p(x)) = (! y. q(y))))";
by (Blast_tac 1);
-(*slower with smaller bounds*)
result();
writeln"Problem 35";