On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote:
Rob,
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".
set_int_control("tactic_subgoal_warning", 35);
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?
Regards,
Rob
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
