clarified symbol groups, despite this traditional arrangement in X-symbol grid;
authorwenzelm
Wed Nov 21 20:50:34 2012 +0100 (2012-11-21)
changeset 501591f645910e177
parent 50158 7b61a539721e
child 50160 a29be9d067d2
clarified symbol groups, despite this traditional arrangement in X-symbol grid;
etc/symbols
     1.1 --- a/etc/symbols	Wed Nov 21 20:36:52 2012 +0100
     1.2 +++ b/etc/symbols	Wed Nov 21 20:50:34 2012 +0100
     1.3 @@ -204,8 +204,8 @@
     1.4  \<rbrace>               code: 0x002984  group: punctuation  abbrev: .}
     1.5  \<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
     1.6  \<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
     1.7 -\<bottom>               code: 0x0022a5  group: arrow
     1.8 -\<top>                  code: 0x0022a4  group: arrow
     1.9 +\<bottom>               code: 0x0022a5  group: operator
    1.10 +\<top>                  code: 0x0022a4  group: operator
    1.11  \<and>                  code: 0x002227  group: operator  abbrev: /\
    1.12  \<And>                  code: 0x0022c0  group: operator  abbrev: !!
    1.13  \<or>                   code: 0x002228  group: operator  abbrev: \/