Re: [isabelle] conflicting versions



I posted a possible answer to this on SO:


http://stackoverflow.com/questions/21194451/conflicting-versions-in-isabelle

I did not want to just copy this answer here on the mailing list, thus just the link.

cheers

chris

On 01/18/2014 10:55 PM, Christian Urban wrote:

I should add that I tested Nominal on my mac machines and
there seems to be no problem with it. Also Gergely can run
successfully the test-suite of Nominal on *his* computer:

   isabelle build -d . -g Tests

completes successfully.

Just when he loads any "nominal" file directly, he gets
into trouble. Unfortunately, I am not a Windows guy to
know what he needs to delete in order to get everything
working (I would have stared with deleting heap files
in my .isabelle directory, but I already suggested this to
Gergely).

Hope this helps,
Christian

On Friday, January 17, 2014 at 11:57:10 (+0100), Buday Gergely wrote:
  > Hi,
  >
  > 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?
  >
  > - Gergely
  >





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