diff -r d91374c90d0c -r 7a6ae107ec3c etc/symbols
--- a/etc/symbols	Fri Jan 01 11:07:07 2016 +0100
+++ b/etc/symbols	Fri Jan 01 11:07:29 2016 +0100
@@ -352,6 +352,8 @@
 \<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