diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/IntDiv.thy
--- 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)>))"