changeset 10543 | 8e4307d1207a |
parent 10539 | 5929460a41df |
child 10595 | be043b89acc5 |
--- 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}