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.


Quoting Jeremy Dawson <jeremy at>:

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

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?



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