etc/symbols

 \<succeq>               code: 0x00227d  group: relation
 \<parallel>             code: 0x002225  group: punctuation  abbrev: ||
 \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
 \<plusminus>            code: 0x0000b1  group: operator
 \<minusplus>            code: 0x002213  group: operator
-\<times>                code: 0x0000d7  group: operator
+\<times>                code: 0x0000d7  group: operator  abbrev: <*>
 \<div>                  code: 0x0000f7  group: operator
 \<cdot>                 code: 0x0022c5  group: operator
 \<star>                 code: 0x0022c6  group: operator
 \<bullet>               code: 0x002219  group: operator
 \<circ>                 code: 0x002218  group: operator