doc-src/TutorialI/tutorial.tex
changeset 10654 458068404143
parent 10597 29dd6ac8c223
child 10676 06f390008ceb
equal deleted inserted replaced
10653:55f33da63366 10654:458068404143
    43 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
    43 \newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
    44 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
    44 \newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
    45 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
    45 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
    46 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
    46 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
    47 
    47 
       
    48 \index{termination|see{total function}}
    48 \index{product type|see{pair}}
    49 \index{product type|see{pair}}
    49 \index{tuple|see{pair}}
    50 \index{tuple|see{pair}}
       
    51 \index{*<*lex*>|see{lexicographic product}}
    50 
    52 
    51 \underscoreoff
    53 \underscoreoff
    52 
    54 
    53 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    55 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    54 
    56