diff -r 71b7a535cf96 -r 4b4b93672f15 etc/symbols
--- a/etc/symbols	Sun Jun 19 00:03:44 2011 +0200
+++ b/etc/symbols	Sun Jun 19 14:11:06 2011 +0200
@@ -353,4 +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