[isabelle-dev] NEWS / CONTRIBUTORS

Lukas Bulwahn bulwahn at in.tum.de
Mon Sep 12 13:41:06 CEST 2011


Thanks for your pointer, Brian.

Code_Char_ord.thy is documented under Code generation.
I added NEWS and CONTRIBUTORS for Cset_Monad, Dlist_Cset, List_Cset, RBT_Mapping.


Lukas


On 09/11/2011 10:39 PM, Brian Huffman wrote:
> On Sun, Sep 11, 2011 at 1:01 PM, Makarius<makarius at sketis.net>  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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list