NEWS: more LaTeX markup

[Makarius]

On 23/12/2024 09:31, Tobias Nipkow wrote:
> 
> I am using these new macros to modify the font for constants. This works very 
> well except for one issue: in latex blocks with line breaks, the \isaindent 
> code does not utilize these macros but includes the bare names only.

This should work better in recent Isabelle/9253dadbd4ac: I had to make 
significant changes to pretty-printing with markup for that. A few more 
changes might be coming a bit later ...


	Makarius