diff -r b98cd131e2b5 -r 5b5656a63bd6 src/HOL/ex/Hex_Bin_Examples.thy
--- a/src/HOL/ex/Hex_Bin_Examples.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Hex_Bin_Examples.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein, NICTA
 *)
 
-section {* Examples for hexadecimal and binary numerals *}
+section \<open>Examples for hexadecimal and binary numerals\<close>
 
 theory Hex_Bin_Examples imports Main 
 begin
@@ -12,10 +12,10 @@
 lemma "0xFF = 255" by (rule refl)
 lemma "0xF = 0b1111" by (rule refl)
 
-text {* 
+text \<open>
   Just like decimal numeral they are polymorphic, for arithmetic 
   they need to be constrained
-*}
+\<close>
 lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
 
 text "The number of leading zeros is irrelevant"
@@ -24,17 +24,17 @@
 text "Unary minus works as for decimal numerals"
 lemma "- 0x0A = - 10" by (rule refl)
 
-text {*
+text \<open>
   Hex and bin numerals are printed as decimal: @{term "0b10"}
-*}
+\<close>
 term "0b10"
 term "0x0A"
 
-text {* 
+text \<open>
   The numerals 0 and 1 are syntactically different from the 
   constants 0 and 1. For the usual numeric types, their values 
   are the same, though.
-*}
+\<close>
 lemma "0x01 = 1" oops 
 lemma "0x00 = 0" oops