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!
Notification Bot (Apr 24 2022 at 16:42):Ciarán Dunne has marked this topic as resolved.
Last updated: Oct 31 2025 at 04:26 UTC