Say I have a theory file full of lemmas. Is there a way to programmatically iterate over all the apply statements and dump/print the proof state (as seen in the right hand pane in Isabelle) at each? I attached a picture. Screen-Shot-2022-04-13-at-09.39.18.png
This is certainly possible but it seems like an Isabelle/Scala task -- there you'd have to retrieve a
Document.Snapshot, filter its commands for the
applys your are looking for, and extract the proof state from the state/command output.
Last updated: Dec 07 2023 at 16:21 UTC