--- 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"