src/HOL/HOLCF/IOA/Traces.thy
changeset 80914 d97fdabd9e2b
parent 63680 6e1e8b5abbfa
--- a/src/HOL/HOLCF/IOA/Traces.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Traces.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -129,7 +129,7 @@
 
 subsubsection \<open>Notions of implementation\<close>
 
-definition ioa_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"  (infixr "=<|" 12)
+definition ioa_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"  (infixr \<open>=<|\<close> 12)
   where "(ioa1 =<| ioa2) \<longleftrightarrow>
     (inputs (asig_of ioa1) = inputs (asig_of ioa2) \<and>
      outputs (asig_of ioa1) = outputs (asig_of ioa2)) \<and>