diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/CTL/PDL.thy
--- a/src/Doc/Tutorial/CTL/PDL.thy	Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/CTL/PDL.thy	Fri Sep 27 23:47:45 2024 +0200
@@ -26,7 +26,7 @@
 \hbox{\<open>valid s f\<close>}. The definition is by recursion over the syntax:
 \<close>
 
-primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   (\<open>(_ \<Turnstile> _)\<close> [80,80] 80)
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   ("(_ \<Turnstile> _)" [80,80] 80)
 where
 "s \<Turnstile> Atom a  = (a \<in> L s)" |
 "s \<Turnstile> Neg f   = (\<not>(s \<Turnstile> f))" |