我是想通过Isar一章来查找Isabelle（定理Prover），第一条语句有。
lemma "¬ surj(f :: 'a ⇒ 'a set)"
我想了解什么是常数 surj 是。我知道，用定理查询很容易。
thm notI
这显示。
(?P ⟹ False) ⟹ ¬ ?P
我试着用谷歌搜索 surj 但没有任何有用的东西出现。
我去查阅了文档(https:/isabelle.in.tum.dedocumentation.html。)但我找不到一个简单的方法来搜索它(例如用搜索栏)。
大家在做证明的时候，如何搜索定义或一般的东西？如何有效地查找伊莎贝尔的东西，而不必为了一些琐碎的东西（我自己可能应该能查到）而求助于SO等？比如一个 man 命令或 -help 标志等？
我发现底部有一个查询框，于是我就试了一下。但是它给我显示了38个定理。Thats good progress BUT I feel that because when I stated my lemma Isabelle knows exactly which one it is using. 有没有办法强迫Isabelle揭示它用的是什么定义（因为它显然必须知道它用的是什么）。
我只是注意到了这一点。
thm surj_def
displays:
surj ?f = (∀y. ∃x. y = ?f x)
确实会显示一些东西......这个问题是值得的，因为我发现了查询框，但无论如何，人们如何在Isabelle中开发还是很不错的。
编辑。
如果能链接到战术的文档，解释他们做了什么或类似的东西，那也会很好......