diff -r 46f59511b7bb -r d97fdabd9e2b src/Doc/Tutorial/CTL/CTL.thy
--- a/src/Doc/Tutorial/CTL/CTL.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/Doc/Tutorial/CTL/CTL.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -35,7 +35,7 @@
 a new datatype and a new function.}
 \<close>
 (*<*)
-primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" (\<open>(_ \<Turnstile> _)\<close> [80,80] 80) where
 "s \<Turnstile> Atom a  =  (a \<in> L s)" |
 "s \<Turnstile> Neg f   = (~(s \<Turnstile> f))" |
 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |