[isabelle-dev] NEWS: Type constraints for constants (inner syntax printing)

[Makarius]

*** General ***

* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
in ML). Most Isabelle theories have been adapted accordingly, such that
hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in
Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.

This refers to Isabelle/8e7bd0566759.


The key change is Isabelle/26ecbac09941, but it only turned out that simple 
due to many "changed for change elimination" before it.

A few more details are still missing, e.g. type constraints for mixfix delimiters.


	Makarius