[isabelle-dev] Where are the error messages?

Dmitriy Traytel traytel at in.tum.de
Wed Apr 3 18:20:11 CEST 2013


Hi,

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.

Dmitriy


More information about the isabelle-dev mailing list