clarified symbol groups, despite this traditional arrangement in X-symbol grid;
authorwenzelm
Wed, 21 Nov 2012 20:50:34 +0100
changeset 50159 1f645910e177
parent 50158 7b61a539721e
child 50160 a29be9d067d2
clarified symbol groups, despite this traditional arrangement in X-symbol grid;
etc/symbols
--- a/etc/symbols	Wed Nov 21 20:36:52 2012 +0100
+++ b/etc/symbols	Wed Nov 21 20:50:34 2012 +0100
@@ -204,8 +204,8 @@
 \<rbrace>               code: 0x002984  group: punctuation  abbrev: .}
 \<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
 \<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
-\<bottom>               code: 0x0022a5  group: arrow
-\<top>                  code: 0x0022a4  group: arrow
+\<bottom>               code: 0x0022a5  group: operator
+\<top>                  code: 0x0022a4  group: operator
 \<and>                  code: 0x002227  group: operator  abbrev: /\
 \<And>                  code: 0x0022c0  group: operator  abbrev: !!
 \<or>                   code: 0x002228  group: operator  abbrev: \/