becomes smaller with every recursive call. There must be exactly one equation

 becomes smaller with every recursive call. There must be exactly one equation

 for each constructor.  Their order is immaterial.

 for each constructor.  Their order is immaterial.

 A more general method for defining total recursive functions is introduced in

 A more general method for defining total recursive functions is introduced in

 \S\ref{sec:recdef}.

 \S\ref{sec:recdef}.

 \input{Misc/document/Tree.tex}%

 \input{Misc/document/Tree.tex}%

 \end{exercise}

 \end{exercise}

 \subsection{Case expressions}

 \subsection{Case expressions}

 \label{sec:case-expressions}

 \label{sec:case-expressions}

 \end{quote}

 \end{quote}

 The heuristic is tricky to apply because it is not obvious that

 The heuristic is tricky to apply because it is not obvious that

 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what

 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what

 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!

 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!

 \section{Case study: compiling expressions}

 \section{Case study: compiling expressions}

 \label{sec:ExprCompiler}

 \label{sec:ExprCompiler}

 {\makeatother\input{CodeGen/document/CodeGen.tex}}

 {\makeatother\input{CodeGen/document/CodeGen.tex}}