src/ZF/Sum.thy

--- a/src/ZF/Sum.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Sum.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -9,7 +9,7 @@
 
 text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>
 
-definition sum :: "[i,i]=>i" (infixr "+" 65) where
+definition sum :: "[i,i]=>i" (infixr \<open>+\<close> 65) where
      "A+B == {0}*A \<union> {1}*B"
 
 definition Inl :: "i=>i" where