Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.
Moved declarations of @QSUM and <*> to a syntax section.
Changed print_translation because <*> is now an infix.

MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle