diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Mon Jun 26 00:23:17 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Mon Jun 26 11:21:49 2000 +0200 @@ -1,3 +1,7 @@ \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: