# HG changeset patch
# User haftmann
# Date 1414074308 -7200
# Node ID d6435f0bf9661e97adacd689d68382c5c2d332e3
# Parent  1b2e7b78a3374d470df5f69516da8b35fd2dfc9b
repaired long-standing accident

diff -r 1b2e7b78a337 -r d6435f0bf966 src/Doc/Tutorial/Inductive/Mutual.thy
--- a/src/Doc/Tutorial/Inductive/Mutual.thy	Thu Oct 23 14:43:51 2014 +0200
+++ b/src/Doc/Tutorial/Inductive/Mutual.thy	Thu Oct 23 16:25:08 2014 +0200
@@ -67,7 +67,7 @@
 
 text{*\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 : 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