# HG changeset patch
# User paulson
# Date 861786048 -7200
# Node ID 84c2178db936a6330498885d19b24de875e4b9d8
# Parent  15763781afb07c81d52041fe0e24856f4c6c1ae8
Fixed typos in comment

diff -r 15763781afb0 -r 84c2178db936 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Wed Apr 23 10:54:22 1997 +0200
+++ b/src/FOL/ex/cla.ML	Wed Apr 23 11:00:48 1997 +0200
@@ -349,8 +349,8 @@
 goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))     \
 \         --> (ALL x. ALL y. q(x,y) <-> q(y,x))";
 by (Blast_tac 1);
-(*Other proofs: Can use Auto_tac(), whidh cheats by using rewriting!  
-  Deepen_tac alone it requires 253 secs.  Or
+(*Other proofs: Can use Auto_tac(), which cheats by using rewriting!  
+  Deepen_tac alone requires 253 secs.  Or
   by (mini_tac 1 THEN Deepen_tac 5 1);
 *)
 result();