NEWS: more LaTeX markup

[Tobias Nipkow]

Thanks Makarius, it works perfectly.

Tobias

On 03/01/2025 20:03, Makarius wrote:
> 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5187 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250104/195bf60a/attachment.bin>