doc-src/TutorialI/Recdef/document/termination.tex
changeset 10654 458068404143
parent 10522 ed3964d1f1a4
child 10795 9e888d60d3e5
     1.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  \noindent
     1.5  Because \isacommand{recdef}'s termination prover involves simplification,
     1.6  we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
     1.7 -a simplification rule:%
     1.8 +a simplification rule:\indexbold{*recdef_simp}%
     1.9  \end{isamarkuptext}%
    1.10  \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    1.11  \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline