src/HOL/ex/cla.ML
changeset 2715 79c35a051196
parent 2575 65abf447151b
child 2891 d8f254ad1ab9
     1.1 --- a/src/HOL/ex/cla.ML	Tue Mar 04 10:19:38 1997 +0100
     1.2 +++ b/src/HOL/ex/cla.ML	Tue Mar 04 10:21:16 1997 +0100
     1.3 @@ -456,7 +456,7 @@
     1.4  by (Fast_tac 1);
     1.5  result();
     1.6  
     1.7 -writeln"Problem 62 as corrected in AAR newletter #31";
     1.8 +writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
     1.9  goal HOL.thy
    1.10      "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
    1.11  \    (ALL x. (~ p a | p x | p(f(f x))) &                        \