| changeset 10654 | 458068404143 |
| parent 10597 | 29dd6ac8c223 |
| child 10676 | 06f390008ceb |
--- 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