//binary operation symbols
  //{input:"-",  tag:"mo", output:"\u0096", tex:null, ttype:CONST},
  {input:"*",  tag:"mo", output:"\u22C5", tex:"cdot", ttype:CONST},
  {input:"**", tag:"mo", output:"\u22C6", tex:"star", ttype:CONST},
  {input:"//", tag:"mo", output:"/",      tex:null, ttype:CONST},
  {input:"\\\\", tag:"mo", output:"\\",   tex:"backslash", ttype:CONST},
  {input:"setminus", tag:"mo", output:"\\", tex:null, ttype:CONST},
  {input:"xx", tag:"mo", output:"\u00D7", tex:"times", ttype:CONST},
  {input:"-:", tag:"mo", output:"\u00F7", tex:"divide", ttype:CONST},
  {input:"@",  tag:"mo", output:"\u2218", tex:"circ", ttype:CONST},
  {input:"o+", tag:"mo", output:"\u2295", tex:"oplus", ttype:CONST},
  {input:"ox", tag:"mo", output:"\u2297", tex:"otimes", ttype:CONST},
  {input:"o.", tag:"mo", output:"\u2299", tex:"odot", ttype:CONST},
  {input:"sum", tag:"mo", output:"\u2211", tex:null, ttype:UNDEROVER},
  {input:"prod", tag:"mo", output:"\u220F", tex:null, ttype:UNDEROVER},
  {input:"^^",  tag:"mo", output:"\u2227", tex:"wedge", ttype:CONST},
  {input:"^^^", tag:"mo", output:"\u22C0", tex:"bigwedge", ttype:UNDEROVER},
  {input:"vv",  tag:"mo", output:"\u2228", tex:"vee", ttype:CONST},
  {input:"vvv", tag:"mo", output:"\u22C1", tex:"bigvee", ttype:UNDEROVER},
  {input:"nn",  tag:"mo", output:"\u2229", tex:"cap", ttype:CONST},
  {input:"nnn", tag:"mo", output:"\u22C2", tex:"bigcap", ttype:UNDEROVER},
  {input:"uu",  tag:"mo", output:"\u222A", tex:"cup", ttype:CONST},
  {input:"uuu", tag:"mo", output:"\u22C3", tex:"bigcup", ttype:UNDEROVER},