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