我想找到定理。我已阅读Isabelle/Isar reference manual中有关find_theorems的部分：
find_theorems条件
从理论或证明上下文中检索与所有给定搜索匹配的事实
标准。准则name: p选择所有完全合格的定理
名称与模式p匹配，模式p可能包含“ *”通配符。条件intro，
elim和dest选择与当前目标匹配的定理作为引言，
消除或销毁规则。条件solves返回
所有可以直接解决当前目标的规则。准则simp: t
选择左侧与给定术语匹配的所有重写规则。的
标准项t选择所有包含模式t的定理-像往常一样，
模式可能包含伪“ _”，原理图变量和
类型约束。
可以在条件前面加上“ -”来选择不匹配的定理。注意
给出空标准列表可得出所有当前已知的事实。一个
可以提供印刷事实数量的可选限制；默认值为40。
默认情况下，重复项将从搜索结果中删除。使用with_dups
显示重复项。
据我了解，Isabelle / jEdit的查找窗口中使用了find_theorems。上面的内容无法帮助我找到以下情况的相关定理（Lambda是Nominal Isabelle扩展的理论。压缩文件是here）：
theory First
imports Lambda
begin
theorem "Lam [x].(Lam [y].(App (Var x)(Var y))) = Lam [y].(Lam [x].(App (Var y)(Var x)))"
当我尝试搜索表达式
Lam Isabelle / jedit说Inner syntax error: unexpected end of input
Failed to parse term
如何查找包含常数
Lam的所有定理？ 最佳答案
由于像普通的lambda（Lam）一样，%本身并不是一个术语，因此您应添加其余部分以获得适当的术语，其中可能包含通配符。在您的示例中，我将执行
find_theorems "Lam [_]. _"
这给出了很多答案。
关于isabelle - 在伊莎贝尔使用“find_theorems”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/21255473/