Re: [isabelle] Goal.prove_future variant of Goal.prove_multi
On Wed, 18 Feb 2015, RenÃ Thiemann wrote:
Yes, as far as I can say on the spot, there could be
Goal.prove_multi_future, but it was never used so far.
In most situations, a plain "map" of Goal.prove should do the same job.
You mainly need Goal.prove_multi for simultaneous induction.
If you do have a convincing application, I can nonetheless add the
missing variant for the next release.
That would indeed be nice. The application we have in mind are the
datatype order/show/... generators. We just recently got a request from
Dmitriy to use the Goal.prove_..._future variants, since the invocation
of the generator on some particular datatype took over 3 minutes which
was blocking the further proceeding of the theory file.
I have refined that here, so it is likely to be in the coming release:
There is also some updated documentation in the same changeset.
This archive was generated by a fusion of
Pipermail (Mailman edition) and