Re: [isabelle] Combining BNF and Quotient

On Friday, March 8, 2013 at 12:03:25 (+0100), Makarius wrote:
 > Concerning Nomimal2, someone was asking about it on the Nominal mailing 
 > list recently: to include some Isabelle application in AFP that depends on 
 > Nomimal2, it has to be available in some official manner.  AFP already has 
 > a "temporary" copy of Nominal2 now, but what is its relation to the main 
 > Nominal2 repository, and its relation to Nominal1 that is part of 
 > Isabelle2013 (and earlier)?

The Nominal2 copy in the AFP is only a stopgap measure.
The hope is to have Nominal2 in the main distribution

Nominal2 is a re-implemntation from the ground up. While 
many ideas are of course the same, the implementations are 
pretty much competely incompatible. Since at least one 
theory in the AFP depends on Nominal1, we have to maintain
for a little while both version. I have no idea what to
do in the long run.

Hope this helps,

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