Added a comment
authorpaulson
Tue Nov 12 11:36:18 1996 +0100 (1996-11-12)
changeset 217308c68550460b
parent 2172 61b806c6dabd
child 2174 0829b7b632c5
Added a comment
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Mon Nov 11 10:55:44 1996 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Nov 12 11:36:18 1996 +0100
     1.3 @@ -568,6 +568,8 @@
     1.4     else (writeln ("Depth = " ^ string_of_int m);
     1.5  	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
     1.6  
     1.7 +(*Search, with depth bound m.  
     1.8 +  This is the "entry point", which does safe inferences first.*)
     1.9  fun safe_depth_tac cs m = 
    1.10    SUBGOAL 
    1.11      (fn (prem,i) =>