src/HOL/ex/cla.ML
changeset 2715 79c35a051196
parent 2575 65abf447151b
child 2891 d8f254ad1ab9
--- 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))) &                        \