diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Fri May 18 16:45:55 2001 +0200
@@ -37,7 +37,7 @@
 example, @{term"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:
 *}
 
 consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"