etc/symbols
changeset 43463 0a2ffb071fca
parent 43455 4b4b93672f15
child 43486 4a1ef71fbf5f
--- 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: -.