equal
deleted
inserted
replaced
194 let fun dpn m st = |
194 let fun dpn m st = |
195 st |> (if has_fewer_prems i st then no_tac |
195 st |> (if has_fewer_prems i st then no_tac |
196 else if m>lim then |
196 else if m>lim then |
197 (warning "Search depth limit exceeded: giving up"; |
197 (warning "Search depth limit exceeded: giving up"; |
198 no_tac) |
198 no_tac) |
199 else (warning ("Search depth = " ^ string_of_int m); |
199 else (priority ("Search depth = " ^ string_of_int m); |
200 tacf m i ORELSE dpn (m+inc))) |
200 tacf m i ORELSE dpn (m+inc))) |
201 in dpn m end; |
201 in dpn m end; |
202 |
202 |
203 (*** Best-first search ***) |
203 (*** Best-first search ***) |
204 |
204 |