NEWS: more LaTeX markup

[Makarius]

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