[isabelle] Goal.prove_future variant of Goal.prove_multi
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and