--- a/src/HOL/HOLCF/IOA/Automata.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Automata.thy Fri Sep 20 19:51:08 2024 +0200
@@ -26,7 +26,7 @@
definition trans_of :: "('a, 's) ioa \<Rightarrow> ('a, 's) transition set"
where "trans_of = fst \<circ> snd \<circ> snd"
-abbreviation trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81, 81, 81, 81] 100)
+abbreviation trans_of_syn (\<open>_ \<midarrow>_\<midarrow>_\<rightarrow> _\<close> [81, 81, 81, 81] 100)
where "s \<midarrow>a\<midarrow>A\<rightarrow> t \<equiv> (s, a, t) \<in> trans_of A"
definition wfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set"
@@ -91,7 +91,7 @@
(outputs a1 \<union> outputs a2),
(internals a1 \<union> internals a2)))"
-definition par :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> ('a, 's * 't) ioa" (infixr "\<parallel>" 10)
+definition par :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> ('a, 's * 't) ioa" (infixr \<open>\<parallel>\<close> 10)
where "(A \<parallel> B) =
(asig_comp (asig_of A) (asig_of B),
{pr. fst pr \<in> starts_of A \<and> snd pr \<in> starts_of B},