diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Wed Dec 06 12:34:40 2000 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Wed Dec 06 13:22:58 2000 +0100 @@ -35,6 +35,7 @@ useful lemmas are shown below. \subsection{Numeric Literals} +\label{sec:numerals} Literals are available for the types of natural numbers, integers and reals and denote integer values of arbitrary size.