【发布时间】：2015-07-16 02:10:07
【问题描述】：
下面给出bad theory import "Multivariate_Analysis"
imports Multivariate_Analysis
导入Main 工作正常，如何导入模块？
【问题讨论】：
标签： isabelle
【发布时间】：2015-07-16 02:10:07
【问题描述】：
对于理论导入，您通常必须指定理论文件的完整或相对路径。所以对于Multivariate_Analysis，这是<path to isabelle distrib>/src/HOL/Multivariate_Analysis/Multivariate_Analysis。仅当理论已经是会话图像的一部分时，才可以省略路径。由于Main 是默认图像HOL 的一部分，因此您可以在没有路径的情况下导入它。从有路径还是没有路径的会话图像中导入理论是否更好，意见不一。
该路径还可能包含$ISABELLE_HOME 或$AFP 等环境变量，用户可以在其本地设置文件中设置这些变量，以便理论适用于不同的安装。对于 Isabelle 发行版中的所有内容，自定义使用 ~~ 作为 Isabelle 发行版文件夹的路径。
总而言之，您的导入应如下所示：
theory My_Theory
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
由于Multivariate_Analysis 是一个相当大的模块，因此更改默认会话图像可能是明智的，这样就不会在每次启动 Isabelle/jEdit 时重新加载所有这些理论。您可以通过在调用时在命令行中指定 -l HOL-Multivariate_Analysis 或通过在理论面板中选择此会话并重新启动 Isabelle/jEdit 来实现。
更新：自 Isabelle2017 以来，最好通过会话名称而不是相对路径名称从其他会话导入理论。那就是
理论Multivariate_Analysis 将被导入为
theory My_Theory
imports "HOL-Multivariate_Analysis.Multivariate_Analysis"
begin
【讨论】：