--- a/doc-src/TutorialI/Types/types.tex Tue Dec 05 18:55:18 2000 +0100 +++ b/doc-src/TutorialI/Types/types.tex Tue Dec 05 18:55:45 2000 +0100 @@ -19,6 +19,8 @@ \section{Numbers} \label{sec:numbers} +\input{Types/numerics} + \index{pair|(} \input{Types/document/Pairs} \index{pair|)}