Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Updated reference to Pelletier erratum
authorpaulson
Tue, 04 Mar 1997 10:21:16 +0100
changeset 2715 79c35a051196
parent 2714 b0fbdfbbad66
child 2716 9e11a914156a
Updated reference to Pelletier erratum
src/FOL/ex/cla.ML file | annotate | diff | comparison | revisions
src/HOL/ex/cla.ML file | annotate | diff | comparison | revisions
src/HOL/ex/mesontest.ML file | annotate | diff | comparison | revisions 
--- 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)))) &                      \
--- 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))) &                        \
--- 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))) &                        \
isabelle