如何使用Isabelle/HOL从源理论文件中自动生成LaTeX？
Isabelle/HOL tutorial.pdf非常漂亮.我将在LaTeX上写一篇论文,里面有很多Isabelle代码.
我是vim粉丝,但只有emacs才有这个Isabelle/HOL环境.jEdit很棒,但我不能使用
using [[simp_trace=true]]
就像在emacs中一样.
如何在jEdit中启用"跟踪" ？
想象一个名为 的 RPM abc-123-1.x86.rpm，我在其中发现了一个错误。
但我不知道如何命名新包。
也许abc-123-2.x86.rpm？但是如果有一个xyz.rpm依赖abc-123-1呢？
也许abc-123-1.x86.1.rpm，...
所以我的问题是RPM 的 Name-Version-Release 的规则是什么？
我有这个C代码:
while(p->next) p = p->next;
我想证明无论列表有多长,当这个循环结束时,p->next等于NULL,EIP引用此循环后的下一条指令.
但我不能.有谁知道如何在Isabelle/HOL中证明循环？