[isabelle] Goal.prove_future variant of Goal.prove_multi



Dear experts,

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.

In complete ignorance of implementation details I have two questions:

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?

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

cheers

chris





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