我怎样才能使用find_theorems搜索整个正式证据档案馆（AFP）的机制？
我已将存档下载到我的计算机上，并且可以从中导入理论。例如，如果我写imports Kleene_Algebra.Kleene_Algebra_Models那么该理论中的所有定理都成功地提供给了我。但如果我然后输入find_theorems <expression>，我只从我导入的特定理论中获得搜索结果。如果我想搜索整个档案怎么办？例如，也许有人证明了一个对我有用的定理，但我不知道他们所说的理论是什么。
find_theorems仅适用于加载的理论。如果您知道定理名称，则可以使用任何文本搜索工具。在 macOS 上，Splotlight 搜索（cmd + 空格）可能很有用。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
