[isabelle-dev] Remaining uses of show_brackets

[Lawrence Paulson]

Yes – exactly and especially when implications are nested.
Larry

> On 10 Oct 2024, at 20:19, Peter Lammich <lammich at in.tum.de> wrote:
> 
> 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;...|]==> 
> 
> 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.
>