--- a/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 10 19:22:05 2015 +0200
@@ -44,17 +44,13 @@
\<close>
definition
- conc :: "['a list, 'a word] \<Rightarrow> 'a word" (infixr "conc" 65)
- where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"
+ conc :: "['a list, 'a word] \<Rightarrow> 'a word" (infixr "\<frown>" 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"
+ iter :: "'a list \<Rightarrow> 'a word" ("(_\<^sup>\<omega>)" [1000])
where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
-notation (xsymbols)
- conc (infixr "\<frown>" 65) and
- iter ("(_\<^sup>\<omega>)" [1000])
-
lemma conc_empty[simp]: "[] \<frown> w = w"
unfolding conc_def by auto