--- a/src/HOL/HOLCF/IOA/Pred.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Pred.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,22 +12,22 @@
 
 type_synonym 'a predicate = "'a \<Rightarrow> bool"
 
-definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  ("_ \<Turnstile> _" [100, 9] 8)
+definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  (\<open>_ \<Turnstile> _\<close> [100, 9] 8)
   where "(s \<Turnstile> P) \<longleftrightarrow> P s"
 
-definition valid :: "'a predicate \<Rightarrow> bool"  ("\<TTurnstile> _" [9] 8)
+definition valid :: "'a predicate \<Rightarrow> bool"  (\<open>\<TTurnstile> _\<close> [9] 8)
   where "(\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
 
-definition Not :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
+definition Not :: "'a predicate \<Rightarrow> 'a predicate"  (\<open>\<^bold>\<not> _\<close> [40] 40)
   where NOT_def: "Not P s \<longleftrightarrow> \<not> P s"
 
-definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<and>" 35)
+definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr \<open>\<^bold>\<and>\<close> 35)
   where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"
 
-definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<or>" 30)
+definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr \<open>\<^bold>\<or>\<close> 30)
   where "(P \<^bold>\<or> Q) s \<longleftrightarrow> P s \<or> Q s"
 
-definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<longrightarrow>" 25)
+definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr \<open>\<^bold>\<longrightarrow>\<close> 25)
   where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s"
 
 end