Coq 有战术语言 Ltac 和匹配设施等等。Isabelle/HOL 是否有一些用于策略的编程语言以及解析、模式匹配等服务？我浏览了 Isabelle 的 Isar 参考手册和旧的 Pawlson 教程，但我找到了线索。
问问题
175 次
1 回答
3
我不是认真的 Isabelle/HOL 用户，所以请谨慎对待。有一种战术语言叫做Eisbach。您可以在论文A Proof Method Language for Isabelle中看到更多信息。ts.data61.csiro.au/publications/nicta_full_text/8465.pdf
于 2019-12-29T12:41:21.657 回答