I tried to define a definition like this:
theory intext
imports ZF.Int
begin
definition zmod :: "[i,i] ⇒ i" (infixl "$//" 69)
where
"a $// b == 0"
However, it shows error in "$//" the "a $// b == 0":
Inner syntax error⌂
Failed to parse prop
I tried to see if there is infix definition in ZF.Int, and I do find it, but the Isabelle shows error in the theory at the beginning:
Cannot update finished theory "ZF.Int"
May I know does anyone has experience in defining definition with infix operator in Isabelle/ZF could give me some advice?
The character / is a special character in mixfix annotations, therefore you need to escape it using ' as follows:
definition zmod :: "[i,i] ⇒ i" (infixl "$'/'/" 69)
where
"a $// b == 0"
For more information regarding mixfix annotations please refer to The Isabelle/Isar Reference Manual, section 8.2.
Regarding the error message Cannot update finished theory "ZF.Int", this means that Int is part of ZF and cannot be edited.