--- a/etc/symbols Tue Aug 13 19:52:12 2013 +0200
+++ b/etc/symbols Tue Aug 13 20:34:46 2013 +0200
@@ -352,8 +352,6 @@
\<some> code: 0x0003f5
\<^sub> code: 0x0021e9 group: control font: IsabelleText abbrev: =_
\<^sup> code: 0x0021e7 group: control font: IsabelleText abbrev: =^
-\<^isub> code: 0x0021e3 group: control font: IsabelleText abbrev: -_
-\<^isup> code: 0x0021e1 group: control font: IsabelleText abbrev: -^
\<^bold> code: 0x002759 group: control font: IsabelleText abbrev: -.
\<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(
\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)