大约 2-3 周前，我开始学习定理证明者 Isabelle。我仍然是一个绝对的初学者，到目前为止我已经学习了教程“Isabelle/HOL 中的编程和证明”。
到目前为止，我发现的对矩阵的唯一帮助是查看 source code in the HOL library .
现在我想学习如何证明矩阵的性质。矩阵的 lambda 语法对我来说仍然很陌生。 是否有关于在 Isabelle 中使用矩阵的教程或基础/中级示例？
最佳答案
这是法新社的最新条目 http://afp.sourceforge.net/entries/Matrix.shtml
CeTA http://cl-informatik.uibk.ac.at/software/ceta/此处作为应用程序引用，因此您可以在那里查找如何在实践中使用它的示例。
关于matrix - 伊莎贝尔:如何使用矩阵，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/16775215/