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