Isabelle Hints

Brackets or No Brackets in jEdit

 

By default jEdit shows goals in the form

A ==> B ==> C
If you instead prefer the style
[| A; B |] ==> C
from the slides, you can enable this in jEdit by adding the line

ISABELLE_JEDIT_OPTIONS="-m brackets"
to the file ~/.isabelle/Isabelle2013/etc/settings. You may have to create this file if it doesn't exist yet.