\RequirePackage{amssymb,amsmath,stmaryrd,alltt,color}

\def\A#1{\mathcal{A}\left\llbracket#1\right\rrbracket}
\def\B#1{\mathcal{B}\left\llbracket#1\right\rrbracket}
\def\N#1{\mathcal{N}\left\llbracket#1\right\rrbracket}
\def\s{s\;}

\def\x{\mathtt{x}}

\def\tt{\mathbf{tt}}
\def\ff{\mathbf{ff}}

\def\AND{\mathtt{\;\&\&\;}}
\def\OR{\mathtt{\;||\;}}

\newcommand{\sdowhile}[2]{\mbox{\texttt{do~}}#1\mbox{\texttt{~while~}}#2}
\def\ruleif#1{\using{\enspace\text{if }#1}}
\def\axif#1{\enspace\text{if }#1}

% Engelbert Hubbers, Annotated Programs
\input{sl1defs}
\newcommand{\pass}[2]{\left[#1\mapsto\calA{#2}\right]}
\newcommand{\smaller}[1]{{\small\textcolor{red}{#1}}}
\renewcommand{\allttsup}[1]{\begin{math}^{\textcolor{red}{#1}}\end{math}}
%\renewcommand{\allttsub}[1]{\begin{math}_{\textcolor{red}{#1}}\end{math}}
\renewcommand{\psqan}[5]{\{#1\}^{\textcolor{red}{#4}}\espace #2 \espace \{#3\}^{\textcolor{red}{#5}}}