# HG changeset patch
# User paulson
# Date 835023107 -7200
# Node ID 8cb50df4957093d797476972e2afbd661f88b067
# Parent  785a7672962e36274710f435a46b7369747df62c
Inserted comment about problem 43

diff -r 785a7672962e -r 8cb50df49570 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Jun 17 16:51:11 1996 +0200
+++ b/src/FOL/ex/cla.ML	Mon Jun 17 16:51:47 1996 +0200
@@ -354,6 +354,8 @@
 by (deepen_tac FOL_cs 5 1);
 (*Faster alternative proof!
         by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1);     
+Can use just deepen_tac but it requires 253 secs?!?
+	by (deepen_tac FOL_cs 0 1);     
 *)
 result();