etc/symbols

 \<acute>                code: 0x0000b4
 \<index>                code: 0x000131
 \<dieresis>             code: 0x0000a8
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
+\<bind>                 code: 0x00291c  abbrev: >>  abbrev: >>=
+\<then>                 code: 0x002aa2  abbrev: >>
 \<some>                 code: 0x0003f5
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<comment>              code: 0x002015  font: IsabelleText
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<