diff -r 8323b8e21fe9 -r 53e32a9b66b8 etc/symbols
--- a/etc/symbols	Sat Nov 07 00:28:42 2015 +0100
+++ b/etc/symbols	Sat Nov 07 12:53:22 2015 +0100
@@ -353,6 +353,7 @@
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<here>                 code: 0x002302  font: IsabelleText
+\<^undefined>           code: 0x002756  group: control  font: IsabelleText
 \<^noindent>            code: 0x0021e4  group: control  font: IsabelleText
 \<^smallskip>           code: 0x002508  group: control  font: IsabelleText
 \<^medskip>             code: 0x002509  group: control  font: IsabelleText