# HG changeset patch
# User wenzelm
# Date 1512425264 -3600
# Node ID 540eeaf88a635696e6617376f500e0524115df71
# Parent  33683164777991a0ecfe0e4c8ac52634f3a80e46
NEWS;

diff -r 336831647779 -r 540eeaf88a63 NEWS
--- a/NEWS	Mon Dec 04 22:56:46 2017 +0100
+++ b/NEWS	Mon Dec 04 23:07:44 2017 +0100
@@ -61,6 +61,12 @@
     isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
     isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
 
+* Named control symbols (without special Unicode rendering) are shown as
+bold-italic keyword. This is particularly useful for the short form of
+antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
+"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
+arguments into this format.
+
 
 *** HOL ***