[isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

[Lawrence Paulson]

> On 15 May 2018, at 14:51, Makarius <makarius at sketis.net> wrote:
> 
> Maybe also a campaign to get rid of unnecessary syntax ambiguity.

Totally. Most of the time it is completely unnecessary