isabelle
-
隐藏运算符以避免 AST 中的歧义
-
Isabelle：不支持通过类型构造函数递归出现数据类型 "Set.set"
-
如何在 Isabelle 文档准备系统中使用主目录文件？
-
使用类型 类 重载构造函数的符号（现在是命名空间问题）
-
类型 class 实例化中的现有常量（例如构造函数）
-
Isabelle 中的可变参数函数
-
使用 Isabelle 简化器重写非相等等价关系
-
如何发现新的引理或猜测或搜索下一个要在 Isabelle 中证明的引理
-
Isabelle/HOL 中的 primrec 和 fun 有什么区别？
-
Isabelle/HOL实际应用示例
-
如何在引理证明后立即制作一个例子来测试 rev_app 。自定义引理的起始示例
-
Isabelle：关于记录的语言环境解释无法证明
-
细化 Isabelle 类型声明
-
为什么 simp 不在 lambda 表达式中处理这个术语？
-
在伊莎贝尔，为什么这个简化引理没有被取代？
-
使自动终止证明使用不同大小的功能
-
伊莎贝尔的双重功能
-
在 Isabelle 中证明拓扑语句
-
用 Isabelle 重写证明一个简单的算术语句
-
'struct' 是否有类似 include 命令，类似于 'sig' 的 'include'？