src/HOL/Library/Omega_Words_Fun.thy

 definition
   conc :: "['a list, 'a word] \<Rightarrow> 'a word"  (infixr \<open>\<frown>\<close> 65)
   where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
 
 definition
-  iter :: "'a list \<Rightarrow> 'a word"  (\<open>(_\<^sup>\<omega>)\<close> [1000])
+  iter :: "'a list \<Rightarrow> 'a word"  (\<open>(\<open>notation=\<open>postfix \<omega>\<close>\<close>_\<^sup>\<omega>)\<close> [1000])
   where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
 
 lemma conc_empty[simp]: "[] \<frown> w = w"
   unfolding conc_def by auto
 

 subsection \<open>Subsequence, Prefix, and Suffix\<close>
 
 definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
   where "suffix k x \<equiv> \<lambda>n. x (k+n)"
 
-definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"  (\<open>_ [_ \<rightarrow> _]\<close> 900)
+definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"
+    (\<open>(\<open>open_block notation=\<open>mixfix subsequence\<close>\<close>_ [_ \<rightarrow> _])\<close> 900)
   where "subsequence w i j \<equiv> map w [i..<j]"
 
 abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
   where "prefix n w \<equiv> subsequence w 0 n"