代码之家 › 专栏 › 技术社区 › tinlyx

如何中止伊莎贝尔的证据?

isabelle

0

tinlyx · 技术社区 · 5 年前

我想知道是否有办法中止伊莎贝尔/杰迪特的证据?

我搜索了“重置”、“中止”等命令,但没有找到。

我知道有 Sorry .但我不确定是否有人使用 很抱歉 ,则假定手头的定理为真或被放弃。而且 很抱歉 似乎不适用于 apply..done 模式

目前,我对我无法证明的定理进行了注释。但是它需要大量的输入(每个(**)中有四个字符)来注释或取消注释,这有点麻烦。

那么,有没有一种标准/通用的方法来中止伊莎贝尔的证据?

0 回复 | 直到 5 年前

1

3

Mathias Fleury 5 年前

首先,命令是 sorry 而且它确实(但仅)在应用风格中起作用:

lemma 
  â¹False â§ Trueâº
  apply (rule conjI)
   apply auto
  sorry

关于实际问题, oops 中止校样,无论是否采用应用样式:

lemma 
  â¹False â§ Trueâº
proof -
  have True
    by auto
  oops

一 哎呀 -无法在以后引用ed证据。