--- a/etc/symbols Mon Feb 17 20:54:03 2014 +0100
+++ b/etc/symbols Mon Feb 17 21:37:41 2014 +0100
@@ -350,6 +350,7 @@
\<newline> code: 0x0023ce
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
+\<here> code: 0x002302 font: IsabelleText
\<^sub> code: 0x0021e9 group: control font: IsabelleText
\<^sup> code: 0x0021e7 group: control font: IsabelleText
\<^bold> code: 0x002759 group: control font: IsabelleText