Reserved Notation "'Ob' a" (at level 50).
Reserved Notation "'Ox' a" (at level 50).
Reserved Notation "sz ''h' a" (at level 50).
Reserved Notation "'Ox' a" (at level 50).
Reserved Notation "l ^+ r" (at level 50, left associativity).
Reserved Notation "l ^* r" (at level 40, left associativity).
Reserved Notation "l ^- r" (at level 50, left associativity).
Reserved Notation "l ^/ r" (at level 50, left associativity).
Reserved Notation "l ^% r" (at level 50, left associativity).
Reserved Notation "l ^| r" (at level 50, left associativity).
Reserved Notation "l ^& r" (at level 40, left associativity).
Reserved Notation "w1 '>s' w2" (at level 70, w2 at next level).
Reserved Notation "w1 '>s=' w2" (at level 70, w2 at next level).
Reserved Notation "w1 '<s' w2" (at level 70, w2 at next level).
Reserved Notation "w1 '<s=' w2" (at level 70, w2 at next level).
Reserved Notation "$ n" (at level 9, n at level 9, format "$ n").
Reserved Notation "# n" (at level 0).
Reserved Notation "l ^<< r" (at level 35).
Reserved Notation "l ^>> r" (at level 35).
Reserved Notation "w ~ 1" (at level 7, left associativity, format "w '~' '1'").
Reserved Notation "w ~ 0" (at level 7, left associativity, format "w '~' '0'").
