equal
deleted
inserted
replaced
454 goal HOL.thy |
454 goal HOL.thy |
455 "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; |
455 "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; |
456 by (Fast_tac 1); |
456 by (Fast_tac 1); |
457 result(); |
457 result(); |
458 |
458 |
459 writeln"Problem 62 as corrected in AAR newletter #31"; |
459 writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; |
460 goal HOL.thy |
460 goal HOL.thy |
461 "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ |
461 "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ |
462 \ (ALL x. (~ p a | p x | p(f(f x))) & \ |
462 \ (ALL x. (~ p a | p x | p(f(f x))) & \ |
463 \ (~ p a | ~ p(f x) | p(f(f x))))"; |
463 \ (~ p a | ~ p(f x) | p(f(f x))))"; |
464 by (Fast_tac 1); |
464 by (Fast_tac 1); |