etc/symbols

 \<dieresis>             code: 0x0000a8
 \<cedilla>              code: 0x0000b8
 \<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