Ciarán Dunne (Apr 19 2022 at 08:30): Ciarán Dunne (Apr 19 2022 at 08:30):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 insert_tac, and global_immediate_proof. Thanks!
Dmitriy Traytel (Apr 19 2022 at 08:32):Doesn't resolve_tac ctxt xs work?
Jan van Brügge (Apr 19 2022 at 08:47):Probably REPEAT_DETERM o resolve_tac ctxt xs if there are multiple subgoals
Ciarán Dunne (Apr 19 2022 at 09:00):Thanks @Jan van Brügge and @Dmitriy Traytel, using the REPEAT_DETERM tactical on resolve did the job!
Last updated: Jul 15 2022 at 23:21 UTC