--- a/src/Doc/Tutorial/Inductive/Mutual.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/Mutual.thy Thu Feb 15 12:11:00 2018 +0100
@@ -67,7 +67,7 @@
text\<open>\noindent Everything works as before, except that
you write \commdx{inductive} instead of \isacommand{inductive\_set} and
-@{prop"evn n"} instead of @{prop"n : Even"}.
+@{prop"evn n"} instead of @{prop"n \<in> Even"}.
When defining an n-ary relation as a predicate, it is recommended to curry
the predicate: its type should be \mbox{@{text"\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool"}}
rather than