* 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
