etc/symbols

 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<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
 \<^medskip>             code: 0x002509  group: document  font: IsabelleText
 \<^bigskip>             code: 0x002501  group: document  font: IsabelleText