hat-2.7.0.0: docs/tutorial1.hva

\newcommand{\highlight}[1]{\red{\tt #1}\black}
\newcommand{\mkblue}[1]{\blue{\tt #1}\black}
\newcommand{\CUT}{\char177}