Stream: Isabelle/ML

Topic: printing proof terms

view this post on Zulip John Scebold (Apr 14 2022 at 13:20):

I have some ML code which takes a lemma and prints out its proof body and all the lemmas used in its proof. However, the output seems to be truncated with a lot of "..." See the screen shot. Any idea how to make ML print the full content? Screen-Shot-2022-04-14-at-08.10.21.png

view this post on Zulip Simon Roßkopf (Apr 14 2022 at 13:37):

You can set ML_print_depth to a higher value, e.g. by declare [[ML_print_depth=10000]]

view this post on Zulip John Scebold (Apr 19 2022 at 17:32):

Setting ML_print_depth worked. I have another related question. 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

Last updated: Dec 07 2023 at 16:21 UTC