diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Inductive/Mutual.thy
--- a/doc-src/TutorialI/Inductive/Mutual.thy	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Mutual.thy	Thu Aug 09 18:12:15 2001 +0200
@@ -25,7 +25,7 @@
 (simply concatenate the names of the sets involved) and has the conclusion
 @{text[display]"(?x \<in> even \<longrightarrow> ?P ?x) \<and> (?y \<in> odd \<longrightarrow> ?Q ?y)"}
 
-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:
 *}