equal
deleted
inserted
replaced
326 *} |
326 *} |
327 |
327 |
328 definition |
328 definition |
329 finals :: "lang \<Rightarrow> lang set" |
329 finals :: "lang \<Rightarrow> lang set" |
330 where |
330 where |
331 "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}" |
331 "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}" |
332 |
332 |
333 |
333 |
334 lemma lang_is_union_of_finals: |
334 lemma lang_is_union_of_finals: |
335 shows "A = \<Union> finals A" |
335 shows "A = \<Union> finals A" |
336 unfolding finals_def |
336 unfolding finals_def |