diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -17,7 +17,7 @@
 instance nat :: "term" ..
 
 axiomatization
-  Zero :: nat    ("0") and
+  Zero :: nat    (\<open>0\<close>) and
   Suc :: "nat => nat" and
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
 where
@@ -46,7 +46,7 @@
 qed
 
 
-definition add :: "nat => nat => nat"    (infixl "+" 60)
+definition add :: "nat => nat => nat"    (infixl \<open>+\<close> 60)
   where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
 
 lemma add_0 [simp]: "0 + n = n"