# HG changeset patch
# User wenzelm
# Date 1308512834 -7200
# Node ID 0a2ffb071fcaeaf9c158ff867c3c8f56bdca40ce
# Parent  7f65a68f8b26ef25ba64d9f2ffcc38d5736dcfda
abbreviations for special control symbols;

diff -r 7f65a68f8b26 -r 0a2ffb071fca etc/symbols
--- a/etc/symbols	Sun Jun 19 21:43:41 2011 +0200
+++ b/etc/symbols	Sun Jun 19 21:47:14 2011 +0200
@@ -353,9 +353,9 @@
 \<hungarumlaut>         code: 0x0002dd
 \<spacespace>           code: 0x002423  font: Isabelle
 \<some>                 code: 0x0003f5  font: Isabelle
-\<^sub>                 code: 0x0021e9
-\<^sup>                 code: 0x0021e7
-\<^isub>                code: 0x0021e3
-\<^isup>                code: 0x0021e1
-\<^bold>                code: 0x002759
+\<^sub>                 code: 0x0021e9  abbrev: =_
+\<^sup>                 code: 0x0021e7  abbrev: =^
+\<^isub>                code: 0x0021e3  abbrev: -_
+\<^isup>                code: 0x0021e1  abbrev: -^
+\<^bold>                code: 0x002759  abbrev: -.