# HG changeset patch
# User wenzelm
# Date 1543410303 -3600
# Node ID 0d84e3db67c205bf4d0f72d47af4577d5d231238
# Parent  dc9a39c3f75dd2b69f7cb6d6cb841655b5952a87
clarified symbol groups;

diff -r dc9a39c3f75d -r 0d84e3db67c2 etc/symbols
--- 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