conflicting versions in Isabelle?

Question

I installed Isabelle 2013-2 onto a Windows machine that already had a 2012 version.

Trying to read Lambda.thy from the Nominal Isabelle distribution (already discussed this on its mailing list) I get

Outer syntax error: command expected,
but identifier atom_decl was found

at

theory Lambda
imports
  "../Nominal2"
begin

atom_decl name

Could a version conflict cause this? How can I fix it then?

Does Isabelle store a state in some files or in the registry?

Answer 1

Note: This has nothing to do with having different Isabelle versions installed at the same time. Moreover, I would consider it correct behaviour, since atom_decl is not defined unless you load the corresponding theory file (see below).

Answer: I tried to reproduce the same situation (on my linux machine). Thus I downloaded Isabelle2013-2 and Nominal2 and installed (i.e., unpacked the tar-files) it into the local directory ~/tmp/.

Then, imitating starting Isabelle/jEdit by clicking on an icon in windows, I started it via

$ ~/tmp/Isabelle2013-2/Isabelle2013-2

getting an empty buffer (Scratch.thy). Then I opened

~/tmp/Nominal2-Isabelle2013-1/Nominal/Ex/Lambda.thy

via File -> Open .... (General note: shouldn't the directory be renamed to Nominal2-Isabelle2013-2?)

At this point I get a popup asking about Auto loading of required files. As long as I do not "answer" this popup (or close it by answering with No), I get exactly the error message you describe above, i.e.,

Outer syntax error: command expected,
but identifier atom_decl was found

If I answer with Yes, all required theories are loaded and thus the command atom_decl will be defined and everything is fine.

atom_decl is defined in nominal_atoms.ML which is used by Nominal2_Base.thy, and thus only defined after loading this theory.