--- a/src/FOL/ex/cla.ML Wed Dec 13 14:14:06 1995 +0100
+++ b/src/FOL/ex/cla.ML Thu Dec 14 12:49:32 1995 +0100
@@ -488,6 +488,14 @@
by (fast_tac FOL_cs 1);
result();
+writeln"Problem 62 as corrected in AAR newletter #31";
+goal FOL.thy
+ "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \
+\ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \
+\ (~p(a) | ~p(f(x)) | p(f(f(x)))))";
+by (fast_tac FOL_cs 1);
+result();
+
writeln"Reached end of file.";
--- a/src/HOL/ex/cla.ML Wed Dec 13 14:14:06 1995 +0100
+++ b/src/HOL/ex/cla.ML Thu Dec 14 12:49:32 1995 +0100
@@ -452,4 +452,12 @@
by (fast_tac HOL_cs 1);
result();
+writeln"Problem 62 as corrected in AAR newletter #31";
+goal HOL.thy
+ "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \
+\ (ALL x. (~ p a | p x | p(f(f x))) & \
+\ (~ p a | ~ p(f x) | p(f(f x))))";
+by (fast_tac HOL_cs 1);
+result();
+
writeln"Reached end of file.";
--- a/src/HOL/ex/mesontest.ML Wed Dec 13 14:14:06 1995 +0100
+++ b/src/HOL/ex/mesontest.ML Thu Dec 14 12:49:32 1995 +0100
@@ -496,6 +496,14 @@
by (safe_meson_tac 1);
result();
+writeln"Problem 62 as corrected in AAR newletter #31";
+goal HOL.thy
+ "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \
+\ (ALL x. (~ p a | p x | p(f(f x))) & \
+\ (~ p a | ~ p(f x) | p(f(f x))))";
+by (safe_meson_tac 1);
+result();
+
writeln"Reached end of file.";
(*26 August 1992: loaded in 277 secs. New Jersey v 75*)