On Mon, 25 Jul 2011, Makarius wrote:
On Sun, 24 Jul 2011, Lukas Bulwahn wrote:
In Isabelle/318ca53e3fbb it works half-way, when the outer execution
context is not a worker task itself, e.g. on the tty.
For tool developers, this means as consequence, we either do not use
Par_List.get_some
I spent a bit of yesterday trying to discover why the standard simpset
was taking forever to simplify a large term I happen to have.
The term is folded down in such a manner that unfolding Let_def will
cause it to grow extremely large, which turns out to be what is
happening. Deleting the