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



It would also solve my problem that I tend to forget to test HOLCF after
changing HOL.

Tobias

Jasmin Blanchette schrieb:
> Am 17.11.2010 um 23:07 schrieb Brian Huffman:
> 
>> It is a more obvious that HOL-Nominal is built in Isabelle/HOL, since
>> "HOL-" is a prefix of its name. (Also, it helps that HOL-Nominal
>> resides in a subdirectory of src/HOL in the distribution, instead of
>> being adjacent to ZF, FOL, etc. which really are distinct logics from
>> HOL.) Maybe the same things could help clear up the confusion with
>> HOLCF? Moving the HOLCF directory would be easy to do. But instead of
>> just "HOLCF", maybe it could be labeled as "HOL-HOLCF", or "HOL-LCF",
>> or "HOL-CF"? I suppose I shouldn't take a name-change lightly, though,
>> since "HOLCF" is a recognized brand. Any suggestions?
> 
> 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".
> 
> Jasmin
> 





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