[isabelle-dev] NEWS: New (co)datatype package is now in Main

[Lawrence Paulson]

Great news! I hope to see a brief announcement paper illustrating some of the new things that can be done. Or did you publish that last year?
Larry

On 21 Jan 2014, at 12:54, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> *** HOL ***
> 
> * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
>  The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
>  "primrec_new", "primcorec", and "primcorecursive" command are now part of
>  "Main".
>  INCOMPATIBILITY.
>  Theory renamings:
>    FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
>    Library/Wfrec.thy ~> Wfrec.thy
>    Library/Zorn.thy ~> Zorn.thy
>    Cardinals/Order_Relation.thy ~> Order_Relation.thy
>    Library/Order_Union.thy ~> Cardinals/Order_Union.thy
>    Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
>    Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
>    Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
>    Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
>    Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
>    BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
>    BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
>    BNF/BNF_Comp.thy ~> BNF_Comp.thy
>    BNF/BNF_Def.thy ~> BNF_Def.thy
>    BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
>    BNF/BNF_GFP.thy ~> BNF_GFP.thy
>    BNF/BNF_LFP.thy ~> BNF_LFP.thy
>    BNF/BNF_Util.thy ~> BNF_Util.thy
>    BNF/Coinduction.thy ~> Coinduction.thy
>    BNF/More_BNFs.thy ~> Library/More_BNFs.thy
>    BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
>    BNF/Examples/* ~> BNF_Examples/*
>  New theories:
>    List_Prefix.thy (split from Library/Sublist.thy)
>    Wellorder_Extension.thy (split from Zorn.thy)
>    Library/Cardinal_Notations.thy
>    Library/BNF_Decl.thy
>    BNF_Examples/Misc_Primcorec.thy
>    BNF_Examples/Stream_Processor.thy
>  Discontinued theory:
>    BNF/BNF.thy
>    BNF/Equiv_Relations_More.thy
> 
> 
> 
> This refers to 01869d711567. This brings the new (co)datatype package where we want it to be for the next release.
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev