[isabelle-dev] JEdit: type constraints no longer printed by default

Steffen Juilf Smolka steffen.smolka at in.tum.de
Fri Jan 11 14:28:36 CET 2013


> There might be corner cases where the change of the display leads to odd effects.  Are there concrete incidents already that need to be reconsidered before the release?

We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer and rely on Type.contstraint to introduce type annotations in terms (this does not work with show_markup set to true).

Also, we got the error "Malformed YXML: multiple results" in certain situations.

Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer.

Steffen


More information about the isabelle-dev mailing list