--- 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"