equal
deleted
inserted
replaced
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); |