diff -r 9a5d5df29e5c -r ffb153ef6366 doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Mon Dec 18 15:00:15 2000 +0100 +++ b/doc-src/TutorialI/basics.tex Mon Dec 18 16:11:53 2000 +0100 @@ -187,7 +187,8 @@ in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as \isa{(x < y)::nat}. The main reason for type constraints are overloaded functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for -a full discussion of overloading. +a full discussion of overloading and Table~\ref{tab:overloading} for the most +important overloaded function symbols. \begin{warn} In general, HOL's concrete syntax tries to follow the conventions of