# HG changeset patch
# User wenzelm
# Date 1376832806 -7200
# Node ID 1835a83309d680ede45a33849b389ccfcdd5bbf1
# Parent  acc495621d728d6401fc59b736e80e4384b6d3b2
discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;

diff -r acc495621d72 -r 1835a83309d6 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: =^(