<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Makarius,<div><br></div><div>Thanks a lot for the work.<br><div><br></div><div><div><blockquote type="cite"><br class="Apple-interchange-newline"><div><div>*** General ***<br><br>* Inner syntax translations now support formal dependencies via commands<br>'syntax_types' or 'syntax_consts'. This is essentially an abstract<br>specification of the effect of 'translations' (or translation functions<br>in ML). Most Isabelle theories have been adapted accordingly, such that<br>hyperlinks work properly e.g. for "['a, 'b] ⇒ 'c" or "⟦A; B⟧ ⟹ C" in<br>Pure, and "∀x∈A. B x" or "∃x∈A. B x" in HOL.<br><br>This refers to Isabelle/8e7bd0566759.<br><br></div></div></blockquote>I guess you wanted to mention this News entry:</div><div><br></div><div><div>* Inner syntax printing now supports type constraints for constants:</div><div>this is guarded by the configuration options "show_consts_markup"</div><div>(default true) and "show_markup" (default true for PIDE interaction).</div><div>Ast translation rules (command 'translations') and mixfix notation work</div><div>with or without such extra constraints, but ML translation functions</div><div>(command 'print_ast_translation') need may need to be changed slightly.</div><div>Rare INCOMPATIBILITY. The Prover IDE displays type constraints for</div><div>constants as for variables, e.g. via C-mouse hovering.</div></div><div><br><blockquote type="cite"><div><div><br>The key change is Isabelle/26ecbac09941, but it only turned out that simple due to many "changed for change elimination" before it.<br><br>A few more details are still missing, e.g. type constraints for mixfix delimiters.<br><br><br></div></div></blockquote>Looking forward to it.</div><div><br></div><div><div><div>Regards,</div><div>Norbert</div><div><br></div><div>--</div><div><br></div><div>Norbert Schirmer (nschirmer@apple.com)</div><div> SEG Formal Verification</div><div><br></div><br class="Apple-interchange-newline"></div><br class="Apple-interchange-newline" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"></div></div></div></body></html>