1.1 --- a/NEWS	Tue Jan 21 13:27:50 2014 +0100
     1.2 +++ b/NEWS	Tue Jan 21 13:51:10 2014 +0100
     1.3 @@ -46,6 +46,51 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
     1.8 +  The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
     1.9 +  "primrec_new", "primcorec", and "primcorecursive" command are now part of
    1.10 +  "Main".
    1.11 +  INCOMPATIBILITY.
    1.12 +  Theory renamings:
    1.13 +    FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
    1.14 +    Library/Wfrec.thy ~> Wfrec.thy
    1.15 +    Library/Zorn.thy ~> Zorn.thy
    1.16 +    Cardinals/Order_Relation.thy ~> Order_Relation.thy
    1.17 +    Library/Order_Union.thy ~> Cardinals/Order_Union.thy
    1.18 +    Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
    1.19 +    Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
    1.20 +    Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
    1.21 +    Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
    1.22 +    Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
    1.23 +    BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
    1.24 +    BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
    1.25 +    BNF/BNF_Comp.thy ~> BNF_Comp.thy
    1.26 +    BNF/BNF_Def.thy ~> BNF_Def.thy
    1.27 +    BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
    1.28 +    BNF/BNF_GFP.thy ~> BNF_GFP.thy
    1.29 +    BNF/BNF_LFP.thy ~> BNF_LFP.thy
    1.30 +    BNF/BNF_Util.thy ~> BNF_Util.thy
    1.31 +    BNF/Coinduction.thy ~> Coinduction.thy
    1.32 +    BNF/More_BNFs.thy ~> Library/More_BNFs.thy
    1.33 +    BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
    1.34 +    BNF/Examples/* ~> BNF_Examples/*
    1.35 +  New theories:
    1.36 +    List_Prefix.thy (split from Library/Sublist.thy)
    1.37 +    Wellorder_Extension.thy (split from Zorn.thy)
    1.38 +    Library/Cardinal_Notations.thy
    1.39 +    Library/BNF_Decl.thy
    1.40 +    BNF_Examples/Misc_Primcorec.thy
    1.41 +    BNF_Examples/Stream_Processor.thy
    1.42 +  Discontinued theory:
    1.43 +    BNF/BNF.thy
    1.44 +    BNF/Equiv_Relations_More.thy
    1.45 +
    1.46 +* New theory:
    1.47 +    Cardinals/Ordinal_Arithmetic.thy
    1.48 +
    1.49 +* Theory reorganizations:
    1.50 +  * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
    1.51 +
    1.52  * The symbol "\<newline>" may be used within char or string literals
    1.53  to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
    1.54