diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/CTL/Base.thy
--- a/src/Doc/Tutorial/CTL/Base.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/CTL/Base.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -12,7 +12,7 @@
 we consider a simple modal logic called propositional dynamic
 logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
 used in many real
-model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
+model checkers. In each case we give both a traditional semantics (\<open>\<Turnstile>\<close>) and a
 recursive function @{term mc} that maps a formula into the set of all states of
 the system where the formula is valid. If the system has a finite number of
 states, @{term mc} is directly executable: it is a model checker, albeit an