# Re: [isabelle] Goal.prove_future variant of Goal.prove_multi

On Tue, 17 Feb 2015, Christian Sternagel wrote:

`in src/Pure/goal.ML there is the Goal.prove_future variant of Goal.prove.
``However I couldn't find a "future" variant of Goal.prove_multi.
`

`Is it just an interface-omission that there is no
``Goal.prove_multi_future or are there technical reasons for not having
``such a variant of Goal.prove_multi?
`

`Yes, as far as I can say on the spot, there could be
``Goal.prove_multi_future, but it was never used so far. The Goal.prove
``variants are relatively pragmatic, e.g. legacy things like
``Goal.prove_global are there, because some packages still need them, and
``thus their implementation is simplified a bit.
`

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

`Why isn't Goal.prove implicitly "futurized"? (So that the standard
``behavior allows for implicit parallelization; I guess that's not always
``a good thing.)
`

`In Isabelle/ML programming there is often a situation where some tool uses
``Goal.prove ... handle ERROR _ => to react on a failed attempt, i.e. there
``is an implicit assumption of strictness of this operation.
`

`There is an ancient Isabelle tradition to change semantics only together
``with the name of an operation, so I left Goal.prove unchanged and added
``Goal.prove_future. It should be easy to upgrade tools that cope with
``forked proofs by searching for Goal.prove and making educated guesses if
``it can be replaced by Goal.prove_future.
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*