etc/symbols
changeset 53021 d0fa3f446b9d
parent 50194 829ce6e03279
child 53073 1835a83309d6
     1.1 --- a/etc/symbols	Tue Aug 13 19:52:12 2013 +0200
     1.2 +++ b/etc/symbols	Tue Aug 13 20:34:46 2013 +0200
     1.3 @@ -352,8 +352,6 @@
     1.4  \<some>                 code: 0x0003f5
     1.5  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText  abbrev: =_
     1.6  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText  abbrev: =^
     1.7 -\<^isub>                code: 0x0021e3  group: control  font: IsabelleText  abbrev: -_
     1.8 -\<^isup>                code: 0x0021e1  group: control  font: IsabelleText  abbrev: -^
     1.9  \<^bold>                code: 0x002759  group: control  font: IsabelleText  abbrev: -.
    1.10  \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
    1.11  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)