--- 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)" |