--- a/etc/symbols Wed Nov 28 14:00:22 2018 +0100
+++ b/etc/symbols Wed Nov 28 14:05:03 2018 +0100
@@ -188,7 +188,7 @@
\<downharpoonright> code: 0x0021c2 group: arrow
\<upharpoonleft> code: 0x0021bf group: arrow
#\<upharpoonright> code: 0x0021be group: arrow
-\<restriction> code: 0x0021be group: punctuation
+\<restriction> code: 0x0021be group: operator
\<Colon> code: 0x002237 group: punctuation
\<up> code: 0x002191 group: arrow
\<Up> code: 0x0021d1 group: arrow
@@ -327,7 +327,7 @@
\<copyright> code: 0x0000a9
\<registered> code: 0x0000ae
\<hyphen> code: 0x002010 group: punctuation
-\<inverse> code: 0x0000af group: punctuation
+\<inverse> code: 0x0000af group: operator
\<onequarter> code: 0x0000bc group: digit
\<onehalf> code: 0x0000bd group: digit
\<threequarters> code: 0x0000be group: digit
@@ -353,8 +353,8 @@
\<dieresis> code: 0x0000a8
\<cedilla> code: 0x0000b8
\<hungarumlaut> code: 0x0002dd
-\<bind> code: 0x00291c abbrev: >>=
-\<then> code: 0x002aa2 abbrev: >>
+\<bind> code: 0x00291c group: operator abbrev: >>=
+\<then> code: 0x002aa2 group: operator abbrev: >>
\<some> code: 0x0003f5
\<hole> code: 0x002311
\<newline> code: 0x0023ce