
diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Inductive/Mutual.thy
--- a/src/Doc/Tutorial/Inductive/Mutual.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/Mutual.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -1,12 +1,12 @@
 (*<*)theory Mutual imports Main begin(*>*)
 
-subsection{*Mutually Inductive Definitions*}
+subsection\<open>Mutually Inductive Definitions\<close>
 
-text{*
+text\<open>
 Just as there are datatypes defined by mutual recursion, there are sets defined
 by mutual induction. As a trivial example we consider the even and odd
 natural numbers:
-*}
+\<close>
 
 inductive_set
   Even :: "nat set" and
@@ -16,7 +16,7 @@
 | EvenI: "n \<in> Odd \<Longrightarrow> Suc n \<in> Even"
 | OddI:  "n \<in> Even \<Longrightarrow> Suc n \<in> Odd"
 
-text{*\noindent
+text\<open>\noindent
 The mutually inductive definition of multiple sets is no different from
 that of a single set, except for induction: just as for mutually recursive
 datatypes, induction needs to involve all the simultaneously defined sets. In
@@ -26,25 +26,25 @@
 
 If we want to prove that all even numbers are divisible by two, we have to
 generalize the statement as follows:
-*}
+\<close>
 
 lemma "(m \<in> Even \<longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<longrightarrow> 2 dvd (Suc n))"
 
-txt{*\noindent
+txt\<open>\noindent
 The proof is by rule induction. Because of the form of the induction theorem,
 it is applied by @{text rule} rather than @{text erule} as for ordinary
 inductive definitions:
-*}
+\<close>
 
 apply(rule Even_Odd.induct)
 
-txt{*
+txt\<open>
 @{subgoals[display,indent=0]}
 The first two subgoals are proved by simplification and the final one can be
 proved in the same manner as in \S\ref{sec:rule-induction}
 where the same subgoal was encountered before.
 We do not show the proof script.
-*}
+\<close>
 (*<*)
   apply simp
  apply simp
@@ -55,17 +55,17 @@
 done
 (*>*)
 
-subsection{*Inductively Defined Predicates\label{sec:ind-predicates}*}
+subsection\<open>Inductively Defined Predicates\label{sec:ind-predicates}\<close>
 
-text{*\index{inductive predicates|(}
+text\<open>\index{inductive predicates|(}
 Instead of a set of even numbers one can also define a predicate on @{typ nat}:
-*}
+\<close>
 
 inductive evn :: "nat \<Rightarrow> bool" where
 zero: "evn 0" |
 step: "evn n \<Longrightarrow> evn(Suc(Suc n))"
 
-text{*\noindent Everything works as before, except that
+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"}.
 When defining an n-ary relation as a predicate, it is recommended to curry
@@ -75,6 +75,6 @@
 
 When should you choose sets and when predicates? If you intend to combine your notion with set theoretic notation, define it as an inductive set. If not, define it as an inductive predicate, thus avoiding the @{text"\<in>"} notation. But note that predicates of more than one argument cannot be combined with the usual set theoretic operators: @{term"P \<union> Q"} is not well-typed if @{text"P, Q :: \<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> bool"}, you have to write @{term"%x y. P x y & Q x y"} instead.
 \index{inductive predicates|)}
-*}
+\<close>
 
 (*<*)end(*>*)




