Email Gateway (Aug 19 2022 at 13:33): Email Gateway (Aug 19 2022 at 13:33):From: Buday Gergely <gbuday@karolyrobert.hu>
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?
Email Gateway (Aug 19 2022 at 13:33):From: Christian Urban <christian.urban@kcl.ac.uk>
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
Email Gateway (Aug 19 2022 at 13:34):From: Christian Sternagel <c.sternagel@gmail.com>
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
Last updated: Apr 26 2024 at 04:17 UTC