在Isabelle中探索已完成的理论
在Isabelle中探索已完成的理论
提问于 2019-03-07 00:56:51
我想看看Isabelle/HOL分布的向量空间理论文件中的定义。Isabelle邮件列表的This thread解释了如何使用命令isabelle make HOL-Base执行此操作。
我在Windows10下工作。我猜上面的命令是针对Linux的。如何才能在我的系统中获得相同的效果？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-04-05 16:26:50
尝试使用isabelle jedit -l Pure从命令行启动Isabelle (命令行工具在Windows下通过Isabelle2018\Cygwin-Terminal.bat调用)。现在使用Isabelle/Pure作为基础映像，而不是Isabelle/HOL。下一步，从Isabelle安装目录中加载您想要检查的理论文件(HOL stuff在<isabelle-dir>/src/HOL下)
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/55028386
复制相关文章
相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号