【发布时间】：2020-02-09 03:06:35
【问题描述】：
我正在尝试使用理论Finite_Set.thy 但是当我导入它时
imports "$ISABELLE_HOME/SRC/HOL/Finite_Set"
我正在研究的理论没有被解析。当我打开理论本身时，我收到以下错误：
无法更新已完成的理论“HOL.Finite_Set”
我不确定这意味着什么（或者是否相关）或者我能做些什么。
【问题讨论】：
【发布时间】：2020-02-09 03:06:35
【问题描述】：
A similar question has already been asked on the Isabelle mailing-list
Finite_Set 是 HOL 的一部分，无法编辑（您无法单击它来打开定义等）。你应该导入 Main (aka HOL.Main) 而不是只导入 Finite_Set。
如果你真的想只导入Finite_Set，你应该通过HOL.Finite_Set导入，而不是给出完整路径。
但是，这不应该是您的问题的原因。
【讨论】：