Re: [isabelle] Setting in Isabelle 2019 to fully parenthesize output?
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
On 10/9/19 1:34 PM, Peter Lammich wrote:
the reference to ProofGeneral is, of course, outdated.
One way to enable the show_brackets option is to put
in your theory file. The output after this command will have show-
brackets mode enabled then.
On Tue, 2019-10-08 at 10:25 -0700, Andy Fingerhut wrote:
I am a new user of Isabelle, and have installed both Mac and Linux
of Isabelle 2019. I understand that this document is marked as an
tutorial on the Isabelle web site:
and thus it may contain some information that does not apply to
I saw the following text in that older tutorial, on page 6:
"A particular problem for novices can be the priority of operators.
are unsure, use additional parentheses. In those cases where Isabelle
echoes your input, you can see which parentheses are dropped — they
superfluous. If you are unsure how to interpret Isabelle’s output
you don’t know where the (dropped) parentheses go, set the Proof
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
archives of this email list, but have not found anything that looks
Is there a way to cause Isabelle 2019 output to fully parenthesize
expressions, so that the order of operations can be determined
knowing anything about operator precedence rules?
This archive was generated by a fusion of
Pipermail (Mailman edition) and