doc-src/TutorialI/Inductive/Mutual.thy
changeset 11494 23a118849801
parent 10884 2995639c6a09
child 12815 1f073030b97a
--- 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:
 *}