src/Provers/classical.ML
changeset 2173 08c68550460b
parent 2066 b9063086ef56
child 2630 7a962f6829ca
--- 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) =>