[isabelle-dev] Infinite loops with output

Aymeric Bouzy abouzy at mpi-inf.mpg.de
Thu May 28 16:01:32 CEST 2015

> On 28 May 2015, at 15:38, Makarius <makarius at sketis.net> wrote:
> Using Isabelle/ML or SML inside Isabelle is a regular isabelle-users activity, so this is off-topic on this mailing list.

Sorry about that, you are right.
> If you use "tracing" instead of "writeln" the front-end gets a chance to survive this massive DNS attack.
> There is some kind of dialog at the bottom of the output window.

This was exactly what I was looking for ! Thanks a lot.

Maybe it could be considered mentioning it in The Isabelle Cookbook in section 2.2 ?


More information about the isabelle-dev mailing list