Как отобразить скобки вокруг предположений в Isabelle/jEdit?

Question

Когда цели отображаются Изабель в ProofGeneral, предположения представляются в виде квадратных скобок следующим образом:

Однако в Isabelle/jEdit это, похоже, изменилось на стрелки мета-импликации:

Хотя я понимаю, что первое несколько нестандартно, мне легче читать. Есть ли способ изменить поведение Isabelle/jEdit для распечатки целей в старом стиле ProofGeneral?

Answer 1

Формат, который Изабель отображает на выходе, определяется "режимами печати" Изабель. В ProofGeneral по умолчанию print_mode включает в себя brackets режим, который выводит скобки вокруг предположений, в то время как jEdit по умолчанию print_mode включает в себя no_brackets, что делает обратное.

Режим печати можно изменить, установив Plugins > Plugin Options > Isabelle/General > Print Mode в brackets и перезапустить jEdit, добавив -m brackets к isabelle jedit командной строки, или путем включения в ваш ~/.isabelle/etc/settings файл:

ISABELLE_JEDIT_OPTIONS="-m brackets"

Это приведет к тому, что jEdit отобразит скобки, такие как ProofGeneral:

Answer 2

1. Войти в Plugins -> Plugin Options -> Isabelle -> General
2. затем введите brackets в поле Режим печати.
3. Щелкните Применить.
4. Затем закройте Изабель и перезапустите ее.

После этого ваши гипотезы должны быть заключены в скобки.