Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis



On Wed, Nov 17, 2010 at 2:38 PM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> The name HOLCF is nice and established, and the main issue is the confusing directory structure. Fixing the directory structure would yield "~~/src/HOL/HOLCF" and "HOL-HOLCF".

Having the heap image named "HOL-HOLCF" sounds good to me; I will
continue to use just the name "HOLCF" in all the internal
documentation, though.

I would also like to address the positioning of HOLCF in the online
documentation. Currently it is listed on each of these pages:

http://isabelle.in.tum.de/documentation.html
http://isabelle.in.tum.de/dist/library/index.html

where all of the other entries are really distinct logics. (Some are
built as extensions of others - ZF extends FOL, for example - but none
are *conservative* extensions like HOLCF.)

Really, HOLCF should be listed next to HOL-Nominal, etc. here:

http://isabelle.in.tum.de/dist/library/HOL/index.html

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.