renamed // to / (which is what we want anyway) to avoid clash with the new
use of // for quotienting
\begin{isabelle}%
~{"}let~(x,y)~=~f~z~in~(y,x){"}~{"}case~xs~of~[]~{\isasymRightarrow}~0~|~(x,y)\#zs~{\isasymRightarrow}~x+y{"}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: