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

[Norbert Schirmer]

Hi Makarius,

Thanks a lot for the work.

> 
> *** 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.
> 
I guess you wanted to mention this News entry:

* Inner syntax printing now supports type constraints for constants:
this is guarded by the configuration options "show_consts_markup"
(default true) and "show_markup" (default true for PIDE interaction).
Ast translation rules (command 'translations') and mixfix notation work
with or without such extra constraints, but ML translation functions
(command 'print_ast_translation') need may need to be changed slightly.
Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
constants as for variables, e.g. via C-mouse hovering.

> 
> 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.
> 
> 
Looking forward to it.

Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241017/304e0bc5/attachment.htm>