Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Setting in Isabelle 2019 to fully parenthesize...

view this post on Zulip Email Gateway (Aug 22 2022 at 20:43):

From: Andy Fingerhut <andy.fingerhut@gmail.com>
Greetings.

I am a new user of Isabelle, and have installed both Mac and Linux versions
of Isabelle 2019. I understand that this document is marked as an old
tutorial on the Isabelle web site:
https://isabelle.in.tum.de/dist/Isabelle2019/doc/tutorial.pdf

and thus it may contain some information that does not apply to Isabelle
2019.

I saw the following text in that older tutorial, on page 6:

"A particular problem for novices can be the priority of operators. If you
are unsure, use additional parentheses. In those cases where Isabelle
echoes your input, you can see which parentheses are dropped — they were
superfluous. If you are unsure how to interpret Isabelle’s output because
you don’t know where the (dropped) parentheses go, set the Proof General
flag Isabelle > Settings > Show Brackets"

I have looked through the settings I could find in the Mac and Linux
versions of Isabelle 2019, and tried doing some Google searches through the
archives of this email list, but have not found anything that looks similar.

Is there a way to cause Isabelle 2019 output to fully parenthesize
expressions, so that the order of operations can be determined without
knowing anything about operator precedence rules?

Thanks,
Andy

1.

view this post on Zulip Email Gateway (Aug 22 2022 at 20:43):

From: Peter Lammich <lammich@in.tum.de>
Hi Andy,

the reference to ProofGeneral is, of course, outdated.
One way to enable the show_brackets option is to put

declare [[show_brackets]]

in your theory file. The output after this command will have show-
brackets mode enabled then.

view this post on Zulip Email Gateway (Aug 22 2022 at 20:43):

From: Dominique Unruh <unruh@ut.ee>
Hi,

and to add to Peter's command:

you can also use "note [[show_brackets]]" inside a "proof ... qed"
proof, and "using [[show_brackets]]" inside a backwards proof (apply
script). This can be useful if you just want to understand one
particular subgoal.

Best wishes,
Dominique.

Last updated: Nov 21 2024 at 12:39 UTC