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



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.