* HOL/Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. This lived hidden in $AFP/Automatic_Refinement before, but other entries started to use it. So I moved it to HOL/Library. (Expecting $AFP/LTL_to_DRA to break until Salomon, who wants to adapt it himself, has fixed it) -- Peter