| changeset 10543 | 8e4307d1207a |
| parent 10524 | 270b285d48ee |
| child 10597 | 29dd6ac8c223 |
--- a/doc-src/TutorialI/tutorial.tex Wed Nov 29 18:42:40 2000 +0100 +++ b/doc-src/TutorialI/tutorial.tex Thu Nov 30 13:56:46 2000 +0100 @@ -45,6 +45,9 @@ \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}} \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}} +\index{product type|see{pair}} +\index{tuple|see{pair}} + \underscoreoff \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???