equal
deleted
inserted
replaced
155 [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), |
155 [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), |
156 (true,subst_prodE) ]; |
156 (true,subst_prodE) ]; |
157 |
157 |
158 (*0 subgoals vs 1 or more*) |
158 (*0 subgoals vs 1 or more*) |
159 val (safe0_brls, safep_brls) = |
159 val (safe0_brls, safep_brls) = |
160 partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
160 List.partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
161 |
161 |
162 fun safestep_tac thms i = |
162 fun safestep_tac thms i = |
163 form_tac ORELSE |
163 form_tac ORELSE |
164 resolve_tac thms i ORELSE |
164 resolve_tac thms i ORELSE |
165 biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE |
165 biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE |