Re: [isabelle] conflicting versions



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.