[isabelle-dev] Remaining uses of show_brackets

[Lawrence Paulson]

Oh, that one. I quite forgot it was there. But it’s occasionally useful when you aren’t sure about operator precedences. Is it hard to support?

Larry

> On 10 Oct 2024, at 19:51, Makarius <makarius at sketis.net> wrote:
> 
> 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)))
>