Re: [isabelle] Failing afp-2015 build



On Tue, 17 Nov 2015, Peter Gammie wrote:

On 17 Nov 2015, at 23:03, Makarius <makarius at sketis.net> wrote:

The ConcurrentIMP session was added before the Isabelle2015 release, where PARALLEL_ALLGOALS was not yet available as canonical shortcut.  Thus it fell into the gap of the historical confusion of what PARALLEL_GOALS really means.

When would one wish to use PARALLEL_GOALS now? (Why not just change its behaviour to that of PARALLEL_ALLGOALS?)

The behaviour and the name should fit together. A tactical that is a parallel version of ALLGOALS should be called like that. If PARALLEL_GOALS had been like PARALLEL_ALLGOALS from the outset, I would have also used that name.


	Makarius




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