diff -r 4a9f76263ece -r 76979adf0b96 etc/symbols
--- 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