伊莎贝尔有矛盾的说法吗？

Question

我在一台已经有2012年版本的Windows机器上安装了Isabelle 2013-2。

尝试从名义的Isabelle发行版中读取Lambda.thy (已经在邮件列表中讨论过这个问题)

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

在…

theory Lambda
imports
  "../Nominal2"
begin

atom_decl name

版本冲突会导致这种情况吗？那我怎么解决呢？

伊莎贝尔是将状态存储在某些文件中还是在注册表中？

Answer 1

注释：，这与同时安装不同的版本无关。此外，我认为这是正确的行为，因为除非加载相应的理论文件，否则不会定义atom_decl (参见下面)。

回答：我尝试复制相同的情况(在我的linux机器上)。因此，我下载了伊莎贝尔2013-2和Nominal2，并将其安装(即解压缩tar-files)到本地目录~/tmp/中。

然后，模仿通过单击windows中的图标启动Isabelle/jEdit，我通过

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

获取一个空缓冲区(Scratch.thy)。然后我打开了

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

通过文件->打开..。(一般注意:不应该将目录重命名为Nominal2-Isabelle2013-2吗？)

此时，我会看到一个弹出窗口，询问自动加载所需的文件。只要我不“回答”这个弹出窗口(或者用No来结束它)，我就会得到您上面描述的错误消息，即，

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

如果我回答是的话，所有所需的理论都会被加载，因此命令atom_decl将被定义，并且一切都很好。

atom_decl是在Nominal2_Base.thy使用的nominal_atoms.ML中定义的，因此只有在加载该理论之后才定义。