Yon*_*har 4 command-line isabelle
如何从命令行验证* .thy文件是有效的Isabelle证明？我猜想在GUI中进行操作就等于看到没有问题/错误/警告等。但是有没有办法从命令行执行此操作？
小智 5
您只需要编写一个小的ROOT文件，然后调用即可isabelle build。例如，如果您想检查理论Foo.thy并进行Bar.thy编译，则可以ROOT使用以下内容创建一个名称为文件的文件：
session Test = HOL +
theories
Foo
Bar
然后可以通过编译完成
isabelle build -d. Test
有关更多详细信息，请参见《 Isabelle系统手册》（第2章）。
| 归档时间： |
|
| 查看次数： |
225 次 |
| 最近记录： |