<div dir='auto'>I think here's a confusion between the attribute that shows all parentheses and the print mode that switches printing of premises from a==>b==>... to [|a;b;...|]==> <div dir="auto"><br></div><div dir="auto">Please do not remove the latter, as it has many users. It makes long subgoals more readable, as you don't have to find the last==> to interpret the goal.</div><div dir="auto"><br></div><div dir="auto">Peter </div></div><div class="gmail_extra"><br><div class="gmail_quote">On 10 Oct 2024 20:51, Makarius <makarius@sketis.net> wrote:<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">On 10/10/2024 20:26, Lawrence Paulson wrote:<br>
> Yes – for anyone who wants their proof states to be legible. I always recommend it to students.</p>
<p dir="ltr">I don't understand what you mean by "legible". How is the following example <br>
legible?</p>
<p dir="ltr">declare [[show_brackets]]<br>
lemma ‹∀x y. P x y ⟶ Q y x›</p>
<p dir="ltr">goal (1 subgoal):<br>
  1. (∀(x y). ((P x y) ⟶ (Q y x)))</p>
<p dir="ltr">The parentheses for the variable bindings are even wrong in the sense of the <br>
formal syntax.<br></p>
<p dir="ltr">> It’s exactly the same principle as having [_,_,_] for lists instead of _::_::_::nil.</p>
<p dir="ltr">I don't understand that either. Can you explain that, please?</p>
<p dir="ltr">If I would understand the principle, I could say if cane be done via PIDE <br>
rendering instead of occasionally bad parentheses.<br></p>
<p dir="ltr"> Makarius</p>
<p dir="ltr">_______________________________________________<br>
isabelle-dev mailing list<br>
isabelle-dev@in.tum.de<br>
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br>
</p>
</blockquote></div><br></div>