--- a/doc-src/TutorialI/Advanced/WFrec.thy Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Mon Nov 27 10:38:43 2000 +0100
@@ -51,7 +51,7 @@
text{*
Lexicographic products of measure functions already go a long
-way. Furthermore you may embedding some type in an
+way. Furthermore you may embed some type in an
existing well-founded relation via the inverse image construction @{term
inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
will never have to prove well-foundedness of any relation composed