[isabelle-dev] Remaining uses of show_brackets

[Makarius]

On 10/10/2024 21:19, Peter Lammich 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.

That is unrelated to the current thread. The time to ask about its "remaining 
uses" it not there yet, but it will come when the proof state output has been 
warped 20 yeards foreward. (That is not going to happen for Isabelle2025.)


	Makarius