diff -r cb9d47632573 -r 2665170f104a doc-src/TutorialI/Misc/document/pairs.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,3 @@
+\begin{isabelle}%
+~{"}let~(x,y)~=~f~z~in~(y,x){"}~{"}case~xs~of~[]~{\isasymRightarrow}~0~|~(x,y)\#zs~{\isasymRightarrow}~x+y{"}\isanewline
+\end{isabelle}%