diff -r 9b09acfb7e06 -r 7cf8b604280f etc/symbols --- a/etc/symbols Thu Oct 15 13:28:36 2015 +0200 +++ b/etc/symbols Thu Oct 15 13:28:48 2015 +0200 @@ -359,7 +359,7 @@ \<^item> code: 0x0025aa group: control font: IsabelleText \<^enum> code: 0x0025b8 group: control font: IsabelleText \<^descr> code: 0x0027a7 group: control font: IsabelleText -\<^emph> code: 0x002217 group: control font: IsabelleText +#\<^emph> code: 0x002217 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText