仅使用一种定义进行简化

Question

Isabelle/HOL 中的简化器（simp）通过使用系统中的所有引理/定理/定义/等进行重写。我知道我们可以从简化器中删除一个定义。例如，像这样：

by (simp del:less_imp_le_nat) 

我只需要使用引理 set_rec 来简化。如何删除简化器中的所有定理，只添加引理 set_rec？

类似：

by (simp del_all del:set_rec) 

Answer 1

您可以使用apply(simp only: set_rec)。