When goals are displayed by Isabelle in ProofGeneral, assumptions are rendered as having brackets around them as so:
In Isabelle/jEdit, however, this seems to have changed to meta-implication arrows:
While I understand the former is somewhat non-standard, I find it much easier to read. Is there a way to modify the behaviour of Isabelle/jEdit to print out goals in the old ProofGeneral style?
The format Isabelle renders its output is determined by Isabelle's "print modes". In ProofGeneral, the default print_mode
includes the brackets
mode, which renders brackets around assumptions, while the default jEdit print_mode
includes no_brackets
, which does the opposite.
The print mode can be changed either by setting Plugins > Plugin Options > Isabelle/General > Print Mode
to brackets
and restarting jEdit, by adding -m brackets
to the isabelle jedit
command line, or by including in your ~/.isabelle/etc/settings
file:
ISABELLE_JEDIT_OPTIONS="-m brackets"
This will result in jEdit displaying brackets like ProofGeneral: