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

[Makarius]

On Tue, 15 Sep 2015, Peter Lammich wrote:

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

This refers to Isabelle/0b071f72f330.  On isabelle-dev postings without 
proper changeset id hardly make any sense.


> (Expecting $AFP/LTL_to_DRA to break until Salomon, who wants to adapt it 
> himself, has fixed it)

This refers to AFP/498eb40c9d9e, where it is so broken that the session 
hierarchy fails utterly.  In other words: total failure of existence. In 
AFP/3085eb9e2bb9, I've formally adjusted the session definitions at least 
-- in much less time than writing this mail.

I guess that it is mostly trivial to adjust the actual theories as well. 
The common practice is that someone who does a change like 0b071f72f330 
above also adjusts all of AFP accordingly, unless there are really big 
problems that need the original author.

The AFP editors have stated a theoretical scheme of maintenance by the 
original authors more than 10 years ago.  If we would have followed that, 
AFP would not be where it is today. Most maintenance happens 
"automagically".


 	Makarius