# HG changeset patch
# User paulson
# Date 857467276 -3600
# Node ID 79c35a0511963bea1150537d0bd49462e2120854
# Parent  b0fbdfbbad66688b962794d549595ff6643d1995
Updated reference to Pelletier erratum

diff -r b0fbdfbbad66 -r 79c35a051196 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Tue Mar 04 10:19:38 1997 +0100
+++ b/src/FOL/ex/cla.ML	Tue Mar 04 10:21:16 1997 +0100
@@ -488,7 +488,7 @@
 by (Fast_tac 1);
 result();
 
-writeln"Problem 62 as corrected in AAR newletter #31";
+writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
 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)))) &                      \
diff -r b0fbdfbbad66 -r 79c35a051196 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Tue Mar 04 10:19:38 1997 +0100
+++ b/src/HOL/ex/cla.ML	Tue Mar 04 10:21:16 1997 +0100
@@ -456,7 +456,7 @@
 by (Fast_tac 1);
 result();
 
-writeln"Problem 62 as corrected in AAR newletter #31";
+writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
 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))) &                        \
diff -r b0fbdfbbad66 -r 79c35a051196 src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Tue Mar 04 10:19:38 1997 +0100
+++ b/src/HOL/ex/mesontest.ML	Tue Mar 04 10:21:16 1997 +0100
@@ -569,7 +569,7 @@
 by (safe_meson_tac 1);
 result();
 
-writeln"Problem 62 as corrected in AAR newletter #31";
+writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
 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))) &                        \