diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Sat Nov 04 18:54:22 2000 +0100 +++ b/doc-src/TutorialI/basics.tex Mon Nov 06 11:32:23 2000 +0100 @@ -186,8 +186,8 @@ \ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed 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:TypeClasses} for -a full discussion of overloading.) +functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for +a full discussion of overloading. \begin{warn} In general, HOL's concrete syntax tries to follow the conventions of