--- a/NEWS Wed Oct 09 23:38:29 2024 +0200
+++ b/NEWS Wed Oct 09 23:59:49 2024 +0200
@@ -23,9 +23,17 @@
re-use: "unbundle no b" etc.
* Blocks for pretty-printing (of types, terms, props etc.) now support
-the option "open_block". Thus the block has no impact on formatting, but
-it may carry markup information, which is relevant both for input and
-output of inner syntax.
+properties "open_block" (bool) and "notation" (string as cartouche).
+When "open_block" is enabled, the block has no impact on formatting, but
+it may carry markup information via "notation". The latter uses formal
+kinds (e.g. "mixfix", "infix", "binder") together with informal words to
+describe the notation. This markup affects both input and output of
+inner syntax --- it can be explored via mouse hovering in the Prover IDE
+as usual (or programmatically by Isabelle/Scala tools). Markup for
+"infix" and "binder" declarations are automatic, but general mixfix
+forms require manual annotations in the theory library. Plenty of
+existing examples may be found in the Isabelle sources by searching for
+"notation=" (without quotes and no extra space).
* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract