diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/CTL/CTLind.thy
--- a/src/Doc/Tutorial/CTL/CTLind.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/CTL/CTLind.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -10,7 +10,7 @@
 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
 model checker for CTL\@. In particular the proof of the
 @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
-simple as one might expect, due to the @{text SOME} operator
+simple as one might expect, due to the \<open>SOME\<close> operator
 involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
 based on an auxiliary inductive definition.
 
@@ -39,7 +39,7 @@
 The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,
 this requires the following
 reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
-the @{text rule_format} directive undoes the reformulation after the proof.
+the \<open>rule_format\<close> directive undoes the reformulation after the proof.
 \<close>
 
 lemma ex_infinite_path[rule_format]:
@@ -53,10 +53,10 @@
 done
 
 text\<open>\noindent
-The base case (@{prop"t = s"}) is trivial and proved by @{text blast}.
+The base case (@{prop"t = s"}) is trivial and proved by \<open>blast\<close>.
 In the induction step, we have an infinite @{term A}-avoiding path @{term f}
 starting from @{term u}, a successor of @{term t}. Now we simply instantiate
-the @{text"\<forall>f\<in>Paths t"} in the induction hypothesis by the path starting with
+the \<open>\<forall>f\<in>Paths t\<close> in the induction hypothesis by the path starting with
 @{term t} and continuing with @{term f}. That is what the above $\lambda$-term
 expresses.  Simplification shows that this is a path starting with @{term t} 
 and that the instantiated induction hypothesis implies the conclusion.
@@ -129,11 +129,11 @@
 done
 
 text\<open>
-The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the
+The \<open>(no_asm)\<close> modifier of the \<open>rule_format\<close> directive in the
 statement of the lemma means
-that the assumption is left unchanged; otherwise the @{text"\<forall>p"} 
+that the assumption is left unchanged; otherwise the \<open>\<forall>p\<close> 
 would be turned
-into a @{text"\<And>p"}, which would complicate matters below. As it is,
+into a \<open>\<And>p\<close>, which would complicate matters below. As it is,
 @{thm[source]Avoid_in_lfp} is now
 @{thm[display]Avoid_in_lfp[no_vars]}
 The main theorem is simply the corollary where @{prop"t = s"},