Stream: Isabelle/ML

Topic: print proof states

view this post on Zulip John Scebold (Apr 21 2022 at 18:11):

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

view this post on Zulip Fabian Huch (Apr 22 2022 at 07:00):

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 21 2024 at 16:20 UTC