diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Program State *}
+section \<open>Program State\<close>
 
 theory State
 imports TypeRel Value
@@ -21,7 +21,7 @@
 definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
 
-type_synonym aheap = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
+type_synonym aheap = "loc \<rightharpoonup> obj"    -- \<open>"@{text heap}" used in a translation below\<close>
 type_synonym locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
 
 type_synonym state = "aheap \<times> locals"      -- "heap, local parameter including This"
@@ -52,7 +52,7 @@
 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
   "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
 
-text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
+text \<open>Make @{text new_Addr} completely specified (at least for the code generator)\<close>
 (*
 definition new_Addr  :: "aheap => loc \<times> val option" where
   "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
@@ -154,7 +154,7 @@
 lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
 by (simp add: c_hupd_def split_beta)
 
-text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
+text \<open>Naive implementation for @{term "new_Addr"} by exhaustive search\<close>
 
 definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
   "gen_new_Addr h n \<equiv>