src/HOL/ex/cla.ML
changeset 3019 ca5a7bbbee6c
parent 2997 86aaab39ebb1
child 3347 4e7dfe8ae41b
equal deleted 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);