# 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))) & \