[isabelle-dev] Remaining uses of show_brackets

[Makarius]

On 10/10/2024 20:26, Lawrence Paulson wrote:
> Yes – for anyone who wants their proof states to be legible. I always recommend it to students.

I don't understand what you mean by "legible". How is the following example 
legible?

declare [[show_brackets]]
lemma ‹∀x y. P x y ⟶ Q y x›

goal (1 subgoal):
  1. (∀(x y). ((P x y) ⟶ (Q y x)))

The parentheses for the variable bindings are even wrong in the sense of the 
formal syntax.


> It’s exactly the same principle as having [_,_,_] for lists instead of _::_::_::nil.

I don't understand that either. Can you explain that, please?

If I would understand the principle, I could say if cane be done via PIDE 
rendering instead of occasionally bad parentheses.


	Makarius