Added a comment
authorpaulson
Tue, 12 Nov 1996 11:36:18 +0100
changeset 2173 08c68550460b
parent 2172 61b806c6dabd
child 2174 0829b7b632c5
Added a comment
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) =>