--- 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}%