Re: [isabelle] Setting in Isabelle 2019 to fully parenthesize output?



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.


On 10/9/19 1:34 PM, Peter Lammich wrote:
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.

--
   Peter




On Tue, 2019-10-08 at 10:25 -0700, Andy Fingerhut wrote:
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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.