Isabelle/ZF 中缀定义问题

Question

我试过这样定义：

theory intext
imports ZF.Int
begin

definition zmod :: "[i,i] ⇒ i" (infixl "$//" 69)
where 
  "a $// b == 0"

但是，它在 "$//" 中显示错误 "a $// b == 0":

Inner syntax error⌂
Failed to parse prop

我试了一下ZF.Int中是否有中缀定义，确实找到了，但是Isabelle一开始就说明理论有误：

Cannot update finished theory "ZF.Int"

请问有谁有在Isabelle/ZF中使用中缀运算符定义定义的经验可以给我一些建议吗？

Answer 1

字符/是mixfix注解中的特殊字符，因此需要使用'转义如下：

definition zmod :: "[i,i] ⇒ i" (infixl "$'/'/" 69)
where 
  "a $// b == 0"

有关 mixfix 注释的更多信息，请参阅 Isabelle/Isar 参考手册，第 8.2 节。

关于错误消息 Cannot update finished theory "ZF.Int"，这意味着 Int 是 ZF 的一部分，无法编辑。

Isabelle/ZF infix definition issue