diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Types/types.tex --- a/doc-src/TutorialI/Types/types.tex Wed Nov 29 18:42:40 2000 +0100 +++ b/doc-src/TutorialI/Types/types.tex Thu Nov 30 13:56:46 2000 +0100 @@ -19,11 +19,9 @@ \section{Numbers} \label{sec:numbers} -\index{product type|(} +\index{pair|(} \input{Types/document/Pairs} -\index{product type|)} -% Check refs to this section to see what is expected of it. -% Mention type unit +\index{pair|)} \section{Records} \label{sec:records}