src/HOL/ex/cla.ML

 result();
 
 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))))";
-by (Blast_tac 1);
-(*slower with smaller bounds*)
+\              ((? x. q(x)) = (! y. p(y))))   =    \
+\             ((? x. ! y. q(x) = q(y))  =          \
+\              ((? x. p(x)) = (! y. q(y))))";
+by (Blast_tac 1);
 result();
 
 writeln"Problem 35";
 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
 by (Blast_tac 1);