diff -r afdabfeb5e94 -r d0fa3f446b9d etc/symbols
--- 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: =_)