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 MHonArc.