src/FOL/ex/cla.ML

--- 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.";