diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/CTL/CTL.thy
--- a/src/Doc/Tutorial/CTL/CTL.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -7,7 +7,7 @@
 The semantics of PDL only needs reflexive transitive closure.
 Let us be adventurous and introduce a more expressive temporal operator.
 We extend the datatype
-@{text formula} by a new constructor
+\<open>formula\<close> by a new constructor
 \<close>
 (*<*)
 datatype formula = Atom "atom"
@@ -98,7 +98,7 @@
 (*>*)
 text\<open>
 All we need to prove now is  @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
-that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
+that @{term mc} and \<open>\<Turnstile>\<close> agree for @{const AF}\@.
 This time we prove the two inclusions separately, starting
 with the easy one:
 \<close>
@@ -123,7 +123,7 @@
 In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
 The rest is automatic, which is surprising because it involves
 finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
-for @{text"\<forall>p"}.
+for \<open>\<forall>p\<close>.
 \<close>
 
 apply(erule_tac x = "p 1" in allE)
@@ -167,7 +167,7 @@
 
 text\<open>\noindent
 Element @{term"n+1::nat"} on this path is some arbitrary successor
-@{term t} of element @{term n} such that @{term"Q t"} holds.  Remember that @{text"SOME t. R t"}
+@{term t} of element @{term n} such that @{term"Q t"} holds.  Remember that \<open>SOME t. R t\<close>
 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
 course, such a @{term t} need not exist, but that is of no
 concern to us since we will only use @{const path} when a
@@ -218,28 +218,28 @@
 holds. However, we first have to show that such a @{term t} actually exists! This reasoning
 is embodied in the theorem @{thm[source]someI2_ex}:
 @{thm[display,eta_contract=false]someI2_ex}
-When we apply this theorem as an introduction rule, @{text"?P x"} becomes
-@{prop"(s, x) \<in> M \<and> Q x"} and @{text"?Q x"} becomes @{prop"(s,x) \<in> M"} and we have to prove
+When we apply this theorem as an introduction rule, \<open>?P x\<close> becomes
+@{prop"(s, x) \<in> M \<and> Q x"} and \<open>?Q x\<close> becomes @{prop"(s,x) \<in> M"} and we have to prove
 two subgoals: @{prop"\<exists>a. (s, a) \<in> M \<and> Q a"}, which follows from the assumptions, and
 @{prop"(s, x) \<in> M \<and> Q x \<Longrightarrow> (s,x) \<in> M"}, which is trivial. Thus it is not surprising that
-@{text fast} can prove the base case quickly:
+\<open>fast\<close> can prove the base case quickly:
 \<close>
 
  apply(fast intro: someI2_ex)
 
 txt\<open>\noindent
 What is worth noting here is that we have used \methdx{fast} rather than
-@{text blast}.  The reason is that @{text blast} would fail because it cannot
+\<open>blast\<close>.  The reason is that \<open>blast\<close> would fail because it cannot
 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
 subgoal is non-trivial because of the nested schematic variables. For
-efficiency reasons @{text blast} does not even attempt such unifications.
-Although @{text fast} can in principle cope with complicated unification
+efficiency reasons \<open>blast\<close> does not even attempt such unifications.
+Although \<open>fast\<close> can in principle cope with complicated unification
 problems, in practice the number of unifiers arising is often prohibitive and
 the offending rule may need to be applied explicitly rather than
 automatically. This is what happens in the step case.
 
 The induction step is similar, but more involved, because now we face nested
-occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
+occurrences of \<open>SOME\<close>. As a result, \<open>fast\<close> is no longer able to
 solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
 show the proof commands but do not describe the details:
 \<close>
@@ -320,7 +320,7 @@
 simpler arguments.
 
 The main theorem is proved as for PDL, except that we also derive the
-necessary equality @{text"lfp(af A) = ..."} by combining
+necessary equality \<open>lfp(af A) = ...\<close> by combining
 @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
 \<close>
 
@@ -439,7 +439,7 @@
 our model checkers.  It is clear that if all sets are finite, they can be
 represented as lists and the usual set operations are easily
 implemented. Only @{const lfp} requires a little thought.  Fortunately, theory
-@{text While_Combinator} in the Library~@{cite "HOL-Library"} provides a
+\<open>While_Combinator\<close> in the Library~@{cite "HOL-Library"} provides a
 theorem stating that in the case of finite sets and a monotone
 function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
 iterated application of @{term F} to~@{term"{}"} until a fixed point is