# HG changeset patch
# User paulson
# Date 847794978 -3600
# Node ID 08c68550460b0132ee1d8bbfe930979e78aee609
# Parent  61b806c6dabd4d88a3e07b320fec6c72618741ed
Added a comment

diff -r 61b806c6dabd -r 08c68550460b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Nov 11 10:55:44 1996 +0100
+++ b/src/Provers/classical.ML	Tue Nov 12 11:36:18 1996 +0100
@@ -568,6 +568,8 @@
    else (writeln ("Depth = " ^ string_of_int m);
 	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
 
+(*Search, with depth bound m.  
+  This is the "entry point", which does safe inferences first.*)
 fun safe_depth_tac cs m = 
   SUBGOAL 
     (fn (prem,i) =>