Geek Answers Handbook

How to display brackets around assumptions in Isabelle / jEdit?

When targets are displayed by Isabelle in ProofGeneral, assumptions are displayed as having brackets around them like this:

ProofGeneral rendering of assumptions

In Isabelle / jEdit, however, this seems to have changed to meta-implication arrows:

jEdit rendering of assumptions

Although I understand that the first is somewhat non-standard, it is much easier for me to read it. Is there a way to change the behavior of Isabelle / jEdit to print goals in the old ProofGeneral style?

+4
source share
1 answer

The Isabelle format indicates that its output is determined by the Isabelle print mode. In ProofGeneral, the default value of print_mode enables brackets , which creates brackets around assumptions, while jEdit print_mode by default, includes no_brackets , which does the opposite.

You can change the print mode by setting Plugins > Plugin Options > Isabelle/General > Print Mode in brackets and restarting jEdit, adding -m brackets to the isabelle jedit command line or including ~/.isabelle/etc/settings in your file:

 ISABELLE_JEDIT_OPTIONS="-m brackets"

This will cause jEdit to display parentheses such as ProofGeneral:

jEdit rendering brackets

+7
source

More articles:


All Articles