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