diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Inductive/document/Mutual.tex
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Thu Aug 09 18:12:15 2001 +0200
@@ -29,7 +29,7 @@
 \ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
 \end{isabelle}
 
-If we want to prove that all even numbers are divisible by 2, we have to
+If we want to prove that all even numbers are divisible by two, we have to
 generalize the statement as follows:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%