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 <[email protected]> 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 > [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
