Suppose I have
xs : thm list and a proof state whose subgoals are the members of
xs. Is there any easy Isabelle/ML way to solve each subgoal? Currently I'm using
resolve_tac ctxt xs work?
REPEAT_DETERM o resolve_tac ctxt xs if there are multiple subgoals
Thanks @Jan van Brügge and @Dmitriy Traytel, using the
REPEAT_DETERM tactical on resolve did the job!
Ciarán Dunne has marked this topic as resolved.
Last updated: Dec 07 2023 at 16:21 UTC