[isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun

Peter Lammich lammich at in.tum.de
Tue Sep 15 11:24:11 CEST 2015

* 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)


More information about the isabelle-dev mailing list