(**************************************************************************)
notation < "mstyle mathsize big color #ff0000 background #0000ff scriptsizemultiplier 0.8 (x)"
(**************************************************************************)
notation < "mstyle mathsize big color #ff0000 background #0000ff scriptsizemultiplier 0.8 (x)"