src/HOL/ex/cla.ML
 changeset 3347 4e7dfe8ae41b parent 3019 ca5a7bbbee6c child 3842 b55686a7b22c
equal inserted replaced
3346:5101517c2614 3347:4e7dfe8ae41b
`   345 writeln"Problem 43!!";`
`   345 writeln"Problem 43!!";`
`   346 goal HOL.thy`
`   346 goal HOL.thy`
`   347     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \`
`   347     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \`
`   348 \ --> (! x. (! y. q x y = (q y x::bool)))";`
`   348 \ --> (! x. (! y. q x y = (q y x::bool)))";`
`   349 by (Blast_tac 1);`
`   349 by (Blast_tac 1);`
`   350 `
`   350 result();`
`   351 `
`   351 `
`   352 writeln"Problem 44";`
`   352 writeln"Problem 44";`
`   353 goal HOL.thy "(! x. f(x) -->                                    \`
`   353 goal HOL.thy "(! x. f(x) -->                                    \`
`   354 \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \`
`   354 \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \`
`   355 \             (? x. j(x) & (! y. g(y) --> h x y))               \`
`   355 \             (? x. j(x) & (! y. g(y) --> h x y))               \`