diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 12:13:53 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 16:45:55 2001 +0200 @@ -39,7 +39,7 @@ example, \isa{measure\ f} is always well-founded, and the lexicographic product of two well-founded relations is again well-founded, which we relied on when defining Ackermann's function above. -Of course the lexicographic product can also be interated:% +Of course the lexicographic product can also be iterated:% \end{isamarkuptext}% \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ contrived\isanewline