Stream: General

Topic: Printing out all subgoals when there are many

Chengsong Tan (Mar 13 2024 at 15:57):

Hi all,

I have a lemma which involves many subgoals (~100).
How do I ask Isabelle to show all of them in the output window instead of hiding later ones like this (which is the default):

1. ...
......
 10. ......
A total of 26 subgoals...

Thanks a lot,
Chengsong

Mathias Fleury (Mar 13 2024 at 15:59):

supply [[goals_limit=100000]]

Beware: printing is slow in Isabelle

Chengsong Tan (Mar 14 2024 at 13:27):

Mathias Fleury said:

supply [[goals_limit=100000]]

Beware: printing is slow in Isabelle

Thanks, Mathias. Is there a way to do this to the subgoals in an Isar proof?
I got the Illegal application of proof command in "state" mode error when pasting the supply [[goals_limit=10000]] snippet in a "state" mode position. But putting it in a "prove" mode position is of no use as all showing up is the single goal that I am focusing on.

Mathias Fleury (Mar 14 2024 at 13:28):

Outside of a proof: declare. Inside: note

Mathias Fleury (Mar 14 2024 at 13:31):

But I have no idea what you mean with "single goal I am focusing on"
image.png

Chengsong Tan (Mar 14 2024 at 13:34):

Screenshot-2024-03-14-at-13.33.26.png

Mathias Fleury said:

But I have no idea what you mean with "single goal I am focusing on"
image.png

I meant this, but now I have note which works nicely!

Mathias Fleury (Mar 14 2024 at 13:42):

At that point you have a single goal…

Last updated: May 02 2024 at 04:18 UTC