src/HOL/ex/cla.ML
 changeset 3019 ca5a7bbbee6c parent 2997 86aaab39ebb1 child 3347 4e7dfe8ae41b
equal inserted replaced
3018:e65b60b28341 3019:ca5a7bbbee6c
279 result();
279 result();
280
280
281 writeln"Problem 34  AMENDED (TWICE!!)";
281 writeln"Problem 34  AMENDED (TWICE!!)";
282 (*Andrews's challenge*)
282 (*Andrews's challenge*)
283 goal HOL.thy "((? x. ! y. p(x) = p(y))  =               \
283 goal HOL.thy "((? x. ! y. p(x) = p(y))  =               \
284 \                   ((? x. q(x)) = (! y. p(y))))   =    \
284 \              ((? x. q(x)) = (! y. p(y))))   =    \
285 \                  ((? x. ! y. q(x) = q(y))  =          \
285 \             ((? x. ! y. q(x) = q(y))  =          \
286 \                   ((? x. p(x)) = (! y. q(y))))";
286 \              ((? x. p(x)) = (! y. q(y))))";
287 by (Blast_tac 1);
287 by (Blast_tac 1);
288 (*slower with smaller bounds*)

289 result();
288 result();
290
289
291 writeln"Problem 35";
290 writeln"Problem 35";
292 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
291 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
293 by (Blast_tac 1);
292 by (Blast_tac 1);