doc-src/TutorialI/basics.tex
changeset 10538 d1bf9ca9008d
parent 10396 5ab08609e6c8
child 10695 ffb153ef6366
     1.1 --- a/doc-src/TutorialI/basics.tex	Wed Nov 29 10:22:38 2000 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Wed Nov 29 13:44:26 2000 +0100
     1.3 @@ -102,7 +102,7 @@
     1.4    which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
     1.5      \isasymFun~$\tau$}.
     1.6  \item[type variables,]\indexbold{type variable}\indexbold{variable!type}
     1.7 -  denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
     1.8 +  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise
     1.9    to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
    1.10    function.
    1.11  \end{description}
    1.12 @@ -183,10 +183,10 @@
    1.13  Despite type inference, it is sometimes necessary to attach explicit
    1.14  \textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
    1.15  \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
    1.16 -\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
    1.17 +\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
    1.18  in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
    1.19  \isa{(x < y)::nat}. The main reason for type constraints are overloaded
    1.20 -functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for
    1.21 +functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
    1.22  a full discussion of overloading.
    1.23  
    1.24  \begin{warn}