NEWS: more LaTeX markup

[Tobias Nipkow]

Sweet, thanks!

Tobias

On 07/01/2025 23:04, Makarius wrote:
> On 07/01/2025 08:40, Tobias Nipkow wrote:
>>
>> Just one more thing: the field names in record updates are not enclosed in any 
>> macro, eg the field "front":
> 
>> Can you wrap them in \isaconst (because the field selector is a function)?
> 
> This turned out quite easy, using mixfix markup for the specific record syntax: 
> https://isabelle-dev.sketis.net/rISABELLE4b739ed65946
> 
> I have also had a look at theory src/HOL/Library/Datatype_Records.thy but its 
> output syntax appears to be somewhat unfinished anyway.
> 
> 
>      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/20250108/aeeb5534/attachment.bin>