src/ZF/Perm.thy

--- a/src/ZF/Perm.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Perm.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
 
 definition
   (*composition of relations and functions; NOT Suppes's relative product*)
-  comp     :: "[i,i]=>i"      (infixr "O" 60)  where
+  comp     :: "[i,i]=>i"      (infixr \<open>O\<close> 60)  where
     "r O s == {xz \<in> domain(s)*range(r) .
                \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"