NEWS
changeset 67145 e77c5bfca9aa
parent 67140 386a31d6d17a
child 67157 d0657c8b7616
     1.1 --- a/NEWS	Wed Dec 06 09:11:27 2017 +0100
     1.2 +++ b/NEWS	Wed Dec 06 14:19:36 2017 +0100
     1.3 @@ -78,6 +78,11 @@
     1.4  tagged as "document" and visible by default. This avoids the application
     1.5  of option "document_tags" to these commands.
     1.6  
     1.7 +* Isabelle names are mangled into LaTeX macro names to allow the full
     1.8 +identifier syntax with underscore, prime, digits. This is relevant for
     1.9 +antiquotations in control symbol notation, e.g. \<^const_name> becomes
    1.10 +\isactrlconstUNDERSCOREname.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14