> On 28 May 2015, at 15:38, Makarius <makar...@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 ? Aymeric _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev