diff -r 55f33da63366 -r 458068404143 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:39:53 2000 +0100
@@ -45,8 +45,10 @@
 \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
 \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
 
+\index{termination|see{total function}}
 \index{product type|see{pair}}
 \index{tuple|see{pair}}
+\index{*<*lex*>|see{lexicographic product}}
 
 \underscoreoff