Re: [isabelle] Nominal logic in Isabelle 2005 / Re: Incompatibilities between releases



Sorry, I'm lost a bit with this thread. But I can say with
authority that Nominal cannot have been part of Isabelle in
2005. The simple reason is that we did not yet have
anything stable about Nominal in 2005 (the first version
came only out in December 2005). Since then much research
has gone into Nominal.

Also, the supporting ML-code of Nominal *cannot* work with
Isabelle 2005, since it uses many features that were
introduced much later. So, with Nominal, unfortunately
you have no choice: you *must* use Isabelle 2008 (at least)
in order to work effectively.

Christian

Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:


I've just been sent some Isabelle theory files, with the information

(quote)
It [ie, one of the theory files sent to me] should work on an earlier
version of Nominal Package on Isabelle 2005.
(end quote)

I can't find any Nominal stuff in Isabelle 2005; in Isabelle 2007 it's at
Isabelle2007/src/HOL/Nominal, but it doesn't seem to be at the
corresponding location in Isabelle2005.

Whereabouts is the Nominal stuff in Isabelle 2005?

Thanks,

Jeremy







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