Also, I would like to request that when using a non-infinite value of the subgoals flag, the message reporting the number of subgoals remaining should be broken out by how many subgoals are remaining at each level. This information is often a better summary of one's position in the proof than just the total number of subgoals remaining.
Also, I would like to request that when using a non-infinite value of the
subgoals
flag, the message reporting the number of subgoals remaining should be broken out by how many subgoals are remaining at each level. This information is often a better summary of one's position in the proof than just the total number of subgoals remaining.(From #44 by @lambdacalculator)