[isabelle-dev] The coming release

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Sep 24 21:46:22 CEST 2013


>> The first release candidates of Isabelle2013-1 will probably happen in the first or second week of October.
> 
> How is the general situation?  And especially the situation for HOL-BNF?

"HOL-BNF" is a long-term construction yard. There happens to be a lot of development these days, but it's coincidental and not motivated by the release. Our main goal was to have "datatype_new", "datatype_new_compat", and "primrec_new" at roughly the same level of functionality as the old package for the release, and we've achieved that a few weeks ago already. The manual ("datatypes.pdf") is in a reasonable shape since last week. That "primcorec" is actually usable and useful since last week is a nice bonus, but the main users of this command are currently people who use the release version anyway (namely, Andreas, Dmitriy, and Johannes).

As far as "HOL-BNF" is concerned, you can branch any time. What doesn't make it in this release will make it into the next one.

Jasmin




More information about the isabelle-dev mailing list