Updated reference to Pelletier erratum
authorpaulson
Tue Mar 04 10:21:16 1997 +0100 (1997-03-04)
changeset 271579c35a051196
parent 2714 b0fbdfbbad66
child 2716 9e11a914156a
Updated reference to Pelletier erratum
src/FOL/ex/cla.ML
src/HOL/ex/cla.ML
src/HOL/ex/mesontest.ML
     1.1 --- a/src/FOL/ex/cla.ML	Tue Mar 04 10:19:38 1997 +0100
     1.2 +++ b/src/FOL/ex/cla.ML	Tue Mar 04 10:21:16 1997 +0100
     1.3 @@ -488,7 +488,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 FOL.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)))) &                      \
     2.1 --- a/src/HOL/ex/cla.ML	Tue Mar 04 10:19:38 1997 +0100
     2.2 +++ b/src/HOL/ex/cla.ML	Tue Mar 04 10:21:16 1997 +0100
     2.3 @@ -456,7 +456,7 @@
     2.4  by (Fast_tac 1);
     2.5  result();
     2.6  
     2.7 -writeln"Problem 62 as corrected in AAR newletter #31";
     2.8 +writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
     2.9  goal HOL.thy
    2.10      "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
    2.11  \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
     3.1 --- a/src/HOL/ex/mesontest.ML	Tue Mar 04 10:19:38 1997 +0100
     3.2 +++ b/src/HOL/ex/mesontest.ML	Tue Mar 04 10:21:16 1997 +0100
     3.3 @@ -569,7 +569,7 @@
     3.4  by (safe_meson_tac 1);
     3.5  result();
     3.6  
     3.7 -writeln"Problem 62 as corrected in AAR newletter #31";
     3.8 +writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
     3.9  goal HOL.thy
    3.10      "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
    3.11  \    (ALL x. (~ p a | p x | p(f(f x))) &                        \