NEWS: more LaTeX markup

[Makarius]

*** Document preparation ***

* LaTeX output from printed entities (types, terms, thms) now contains
additional markup as follows:

   tclass    -- type class "a"
   tconst    -- type constructor "a"
   tfree     -- free type variable "'a"
   tvar      -- schematic type variable "?'a"
   const     -- constant "a"
   free      -- free variable "a"
   bound     -- bound variable "a"
   skolem    -- skolem variable "a"
   var       -- schematic variable "?a"

These markup names are turned into LaTeX macros using the prefix "\isa",
e.g. "\isaconst{...}" for "const". By default, these macros have no
effect, but may be defined in root.tex like this:

   \renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
   \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}


This refers to Isabelle/f8b28356ab94.

It has required many decades to get to that point: I now recallthat in the 
late 1990ies, we could only get free/bound/var etc. but not the consts. Thanks 
to major cleanup of the inner-syntax framework some months ago, this now 
turned out reasonably easy.


	Makarius