diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,11 +3,11 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Example MicroJava Program *}
+section \<open>Example MicroJava Program\<close>
 
 theory Example imports SystemClasses Eval begin
 
-text {* 
+text \<open>
 The following example MicroJava program includes:
  class declarations with inheritance, hiding of fields, and overriding of
   methods (with refined result type), 
@@ -34,15 +34,15 @@
   }
 }
 \end{verbatim}
-*}
+\<close>
 
 datatype cnam' = Base' | Ext'
 datatype vnam' = vee' | x' | e'
 
-text {*
+text \<open>
   @{text cnam'} and @{text vnam'} are intended to be isomorphic 
   to @{text cnam} and @{text vnam}
-*}
+\<close>
 
 axiomatization cnam' :: "cnam' => cname"
 where
@@ -378,7 +378,7 @@
 apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;"
 apply  (rule t) -- "Expr"
 apply  (rule t) -- "LAss"
-apply    simp -- {* @{text "e \<noteq> This"} *}
+apply    simp -- \<open>@{text "e \<noteq> This"}\<close>
 apply    (rule t) -- "LAcc"
 apply     (simp (no_asm))
 apply    (simp (no_asm))