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);`