--- a/src/ZF/IntDiv.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IntDiv.thy Thu Jan 03 21:15:52 2019 +0100
@@ -88,11 +88,11 @@
else negateSnd (posDivAlg (<$-a,$-b>))"
definition
- zdiv :: "[i,i]=>i" (infixl "zdiv" 70) where
+ zdiv :: "[i,i]=>i" (infixl \<open>zdiv\<close> 70) where
"a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
definition
- zmod :: "[i,i]=>i" (infixl "zmod" 70) where
+ zmod :: "[i,i]=>i" (infixl \<open>zmod\<close> 70) where
"a zmod b == snd (divAlg (<intify(a), intify(b)>))"