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