[isabelle-dev] Where are the error messages?

Makarius makarius at sketis.net
Wed Apr 3 19:22:47 CEST 2013

On Wed, 3 Apr 2013, Dmitriy Traytel wrote:

> theory Scratch
> imports Main
> begin
> term "True x"
> thm "TrueI[OF TrueI]"
> end
> behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands 
> there is no indication of errors (except of the absence of a popup). This 
> seams to apply to all Isar commands involving Toplevel.no_timing.

This is bad.  I will take a look as soon as possible.

If you need a quick workaround, you can set parallel proofs to 0 in 


More information about the isabelle-dev mailing list