# HG changeset patch
# User paulson
# Date 818941772 -3600
# Node ID 57c3f6d2e69264814e7fc2022fe226dc4bbd1621
# Parent  cdfa3ffcead2edab9aa3c9f202e0703777316c66
Added Pelletier's problem 62, as corrected in AAR
Newletter #31

diff -r cdfa3ffcead2 -r 57c3f6d2e692 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.";
 
diff -r cdfa3ffcead2 -r 57c3f6d2e692 src/HOL/ex/cla.ML
--- 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.";
diff -r cdfa3ffcead2 -r 57c3f6d2e692 src/HOL/ex/mesontest.ML
--- 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*)