equal
deleted
inserted
replaced
14 J. Functional Programming. |
14 J. Functional Programming. |
15 *} |
15 *} |
16 |
16 |
17 method_setup depth_solve = {* |
17 method_setup depth_solve = {* |
18 Method.thms_args (fn thms => Method.METHOD (fn facts => |
18 Method.thms_args (fn thms => Method.METHOD (fn facts => |
19 (DEPTH_SOLVE (HEADGOAL (ares_tac (PolyML.print (facts @ thms))))))) |
19 (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))) |
20 *} "" |
20 *} "" |
21 |
21 |
22 method_setup depth_solve1 = {* |
22 method_setup depth_solve1 = {* |
23 Method.thms_args (fn thms => Method.METHOD (fn facts => |
23 Method.thms_args (fn thms => Method.METHOD (fn facts => |
24 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))) |
24 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))) |