*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Nominal logic in Isabelle 2005 / Re: Incompatibilities between releases*From*: Christian Urban <urbanc at in.tum.de>*Date*: Wed, 08 Oct 2008 04:36:53 +0200*Cc*: curban at cs.princeton.edu, isabelle-users at cl.cam.ac.uk, Alexander Krauss <krauss at in.tum.de>*In-reply-to*: <48EC0FCB.5080309@rsise.anu.edu.au>*References*: <183f54960809230415x3fe54d8fv576e130a98001fae@mail.gmail.com> <1222246210.3005.18.camel@weber> <48DAD6B9.2000709@rsise.anu.edu.au> <48DC4817.20205@in.tum.de> <48EC0FCB.5080309@rsise.anu.edu.au>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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

**References**:

- Previous by Date: [isabelle] Nominal logic in Isabelle 2005 / Re: Incompatibilities between releases
- Next by Date: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Previous by Thread: [isabelle] Nominal logic in Isabelle 2005 / Re: Incompatibilities between releases
- Next by Thread: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list