Corrected a comment in #34
authorpaulson
Tue, 28 May 1996 11:16:38 +0200
changeset 1768 b5272bf9e1a4
parent 1767 0c8f131eac40
child 1769 abdab44dcb8b
Corrected a comment in #34
src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri May 24 12:27:04 1996 +0200
+++ b/src/HOL/ex/cla.ML	Tue May 28 11:16:38 1996 +0200
@@ -276,7 +276,7 @@
 by (best_tac HOL_cs 1);
 result();
 
-writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
+writeln"Problem 34  AMENDED (TWICE!!)";
 (*Andrews's challenge*)
 goal HOL.thy "((? x. ! y. p(x) = p(y))  =               \
 \                   ((? x. q(x)) = (! y. p(y))))   =    \