equal
deleted
inserted
replaced
77 biresolve_tac (safe0_brls @ safep_brls); |
77 biresolve_tac (safe0_brls @ safep_brls); |
78 |
78 |
79 (*One safe or unsafe step. *) |
79 (*One safe or unsafe step. *) |
80 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
80 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
81 |
81 |
82 fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, |
82 fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i]; |
83 biresolve_tac haz_dup_brls i]; |
|
84 |
83 |
85 (*Dumb but fast*) |
84 (*Dumb but fast*) |
86 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
85 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
87 |
86 |
88 (*Slower but smarter than fast_tac*) |
87 (*Slower but smarter than fast_tac*) |