discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
authorwenzelm
Sun, 18 Aug 2013 15:33:26 +0200
changeset 53073 1835a83309d6
parent 53072 acc495621d72
child 53074 e62c7a4b6697
discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
etc/symbols
--- a/etc/symbols	Sun Aug 18 15:31:12 2013 +0200
+++ b/etc/symbols	Sun Aug 18 15:33:26 2013 +0200
@@ -350,9 +350,9 @@
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
-\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText  abbrev: =_
-\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText  abbrev: =^
-\<^bold>                code: 0x002759  group: control  font: IsabelleText  abbrev: -.
+\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
+\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
+\<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(