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<[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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
