Re: [isabelle-dev] Interrupt exceptions using the Par_List combinator get_some

2011-08-10 Thread Makarius
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

[isabelle-dev] Probable bug in let_simp simproc

2011-08-10 Thread Thomas Sewell
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