--- a/etc/symbols Mon Dec 12 17:40:06 2016 +0100
+++ b/etc/symbols Tue Dec 13 11:51:42 2016 +0100
@@ -361,7 +361,7 @@
\<comment> code: 0x002015 group: document font: IsabelleText
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
-\<here> code: 0x002302 font: IsabelleText
+\<^here> code: 0x002302 font: IsabelleText
\<^undefined> code: 0x002756 font: IsabelleText
\<^noindent> code: 0x0021e4 group: document font: IsabelleText
\<^smallskip> code: 0x002508 group: document font: IsabelleText