doc-src/TutorialI/tutorial.tex
changeset 10654 458068404143
parent 10597 29dd6ac8c223
child 10676 06f390008ceb
     1.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -45,8 +45,10 @@
     1.4  \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
     1.5  \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
     1.6  
     1.7 +\index{termination|see{total function}}
     1.8  \index{product type|see{pair}}
     1.9  \index{tuple|see{pair}}
    1.10 +\index{*<*lex*>|see{lexicographic product}}
    1.11  
    1.12  \underscoreoff
    1.13