John Scebold (Apr 14 2022 at 13:20): 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
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]]
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: Apr 19 2024 at 16:20 UTC