repaired long-standing accident
authorhaftmann
Thu Oct 23 16:25:08 2014 +0200 (2014-10-23)
changeset 58774d6435f0bf966
parent 58773 1b2e7b78a337
child 58775 9cd64a66a765
child 58779 aeba9ae93dd8
repaired long-standing accident
src/Doc/Tutorial/Inductive/Mutual.thy
     1.1 --- a/src/Doc/Tutorial/Inductive/Mutual.thy	Thu Oct 23 14:43:51 2014 +0200
     1.2 +++ b/src/Doc/Tutorial/Inductive/Mutual.thy	Thu Oct 23 16:25:08 2014 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  
     1.5  text{*\noindent Everything works as before, except that
     1.6  you write \commdx{inductive} instead of \isacommand{inductive\_set} and
     1.7 -@{prop"evn n"} instead of @{prop"n : even"}.
     1.8 +@{prop"evn n"} instead of @{prop"n : Even"}.
     1.9  When defining an n-ary relation as a predicate, it is recommended to curry
    1.10  the predicate: its type should be \mbox{@{text"\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool"}}
    1.11  rather than