1.1 --- a/etc/symbols	Sun Jun 19 21:43:41 2011 +0200
     1.2 +++ b/etc/symbols	Sun Jun 19 21:47:14 2011 +0200
     1.3 @@ -353,9 +353,9 @@
     1.4  \<hungarumlaut>         code: 0x0002dd
     1.5  \<spacespace>           code: 0x002423  font: Isabelle
     1.6  \<some>                 code: 0x0003f5  font: Isabelle
     1.7 -\<^sub>                 code: 0x0021e9
     1.8 -\<^sup>                 code: 0x0021e7
     1.9 -\<^isub>                code: 0x0021e3
    1.10 -\<^isup>                code: 0x0021e1
    1.11 -\<^bold>                code: 0x002759
    1.12 +\<^sub>                 code: 0x0021e9  abbrev: =_
    1.13 +\<^sup>                 code: 0x0021e7  abbrev: =^
    1.14 +\<^isub>                code: 0x0021e3  abbrev: -_
    1.15 +\<^isup>                code: 0x0021e1  abbrev: -^
    1.16 +\<^bold>                code: 0x002759  abbrev: -.
    1.17