diff -r b98cd131e2b5 -r 5b5656a63bd6 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -2,13 +2,13 @@
     Author: Tjark Weber
 *)
 
-section {* Arithmetic *}
+section \<open>Arithmetic\<close>
 
 theory Arith_Examples
 imports Main
 begin
 
-text {*
+text \<open>
   The @{text arith} method is used frequently throughout the Isabelle
   distribution.  This file merely contains some additional tests and special
   corner cases.  Some rather technical remarks:
@@ -26,12 +26,12 @@
   at the moment (namely inequalities only).  (On the other hand, it
   does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
   does not do.)
-*}
+\<close>
 
 
-subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
+subsection \<open>Splitting of Operators: @{term max}, @{term min}, @{term abs},
            @{term minus}, @{term nat}, @{term Divides.mod},
-           @{term divide} *}
+           @{term divide}\<close>
 
 lemma "(i::nat) <= max i j"
   by linarith
@@ -72,7 +72,7 @@
 lemma "abs (abs (i::int)) = abs i"
   by linarith
 
-text {* Also testing subgoals with bound variables. *}
+text \<open>Also testing subgoals with bound variables.\<close>
 
 lemma "!!x. (x::nat) <= y ==> x - y = 0"
   by linarith
@@ -131,7 +131,7 @@
   by linarith
 
 
-subsection {* Meta-Logic *}
+subsection \<open>Meta-Logic\<close>
 
 lemma "x < Suc y == x <= y"
   by linarith
@@ -140,7 +140,7 @@
   by linarith
 
 
-subsection {* Various Other Examples *}
+subsection \<open>Various Other Examples\<close>
 
 lemma "(x < Suc y) = (x <= y)"
   by linarith
@@ -151,8 +151,8 @@
 lemma "(x::nat) < y & y < z ==> x < z"
   by linarith
 
-text {* This example involves no arithmetic at all, but is solved by
-  preprocessing (i.e. NNF normalization) alone. *}
+text \<open>This example involves no arithmetic at all, but is solved by
+  preprocessing (i.e. NNF normalization) alone.\<close>
 
 lemma "(P::bool) = Q ==> Q = P"
   by linarith
@@ -210,7 +210,7 @@
 (* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
 oops
 
-text {* Constants. *}
+text \<open>Constants.\<close>
 
 lemma "(0::nat) < 1"
   by linarith
@@ -224,13 +224,13 @@
 lemma "(47::int) + 11 < 8 * 15"
   by linarith
 
-text {* Splitting of inequalities of different type. *}
+text \<open>Splitting of inequalities of different type.\<close>
 
 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
   a + b <= nat (max (abs i) (abs j))"
   by linarith
 
-text {* Again, but different order. *}
+text \<open>Again, but different order.\<close>
 
 lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
   a + b <= nat (max (abs i) (abs j))"