On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote:
Can you tell me how can I increase the default subgoal limit when
stripping a goal?
In that proof I sent you an example, or me, the complete version
of the proof creates over 34 subgoals, then, ProofPower give me
a warning telling that the proof reached the limit, and asking
me if I want to continue, entering "y".
or 40 or whatever you want. However, don't set the limit much bigger
than the number of subgoals yo are prepared to deal with. If you set
the limit high and a tactic produces 100s or 1000s of subgoals, the
subgoal package could waste a lot of your time processing those
subgoals and you won't know that there are an intractable number of
subgoals until it has finished.
I think it would be better if the subgoal package just told you there
were lots of subgoals and then carried on trying to process them
rather than output the warning - you can always interrupt it if you
don't want to wait. Does anyone else have any views on this?
Proofpower mailing list