以下给出 bad theory import "Multivariate_Analysis"
imports Multivariate_Analysis
导入Main工作正常,如何导入模块？
对于理论导入,通常必须指定理论文件的完整路径或相对路径.所以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