--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Dec 19 13:58:12 2017 +0100
@@ -222,7 +222,7 @@
by smt+
-section {* Natural numbers *}
+section \<open>Natural numbers\<close>
declare [[smt_nat_as_int]]