| changeset 76231 | 8a48e18f081e |
| parent 76063 | 24c9f56aa035 |
| child 81142 | 6ad2c917dd2e |
--- a/src/HOL/Library/Omega_Words_Fun.thy Fri Sep 30 21:03:58 2022 +0200 +++ b/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 01 07:56:53 2022 +0000 @@ -108,7 +108,7 @@ lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>" - by (rule ext) (simp add: conc_def mod_geq) + by (simp add: fun_eq_iff mod_if) subsection \<open>Subsequence, Prefix, and Suffix\<close>