\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: