On Sun, Sep 11, 2011 at 1:01 PM, Makarius <[email protected]> wrote: > My impression is that NEWS and CONTRIBUTORS for the coming release is still > somewhat incomplete. > > NEWS is not just for bad news -- infamous INCOMPATIBILITY entries -- but for > any "user-relevant changes". If things are not user-relevant then what is > the point of doing them in the first place?
Certainly, any additions to HOL/Library are user-relevant and should be considered NEWS-worthy. A quick comparison of the directory listings for HOL/Library shows that these files are new since Isabelle2011: Code_Char_ord.thy Cset_Monad.thy Dlist_Cset.thy Extended_Nat.thy Extended_Real.thy List_Cset.thy Old_Recdef.thy Product_Lattice.thy Quotient_Set.thy RBT_Mapping.thy Saturated.thy Wfrec.thy A few of these have NEWS entries already (Extended_Nat, Old_Recdef, Saturated, Wfrec). The authors of all the others (this includes me!) should make sure to document each one in the NEWS file. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
