Isabelle 是否弃用了假设放电的规则方法？

Question

我借此机会宣传this webpage很好地解释了规则、规则、规则和规则的内部运作。

但是，我注意到方法 rule(k) 似乎在当前的 Isabelle 中不起作用（与例如 drule(k) 相比。举个例子：

引理“A ⟹ A ∨ B” 应用（规则（1）disjI1）

Answer 1

Isabelle 2020 手册 (Isar-ref) 第 9.2 节指出，方法 rule 只接受一个参数 thms。但是，erule、drule 和 frule 方法有一个额外的可选参数 (nat)：

可选的自然数参数（默认为 0）指定额外的 假设步骤在这里执行。