diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/NanoJava/Term.thy	Thu May 26 17:51:22 2016 +0200
@@ -6,16 +6,16 @@
 
 theory Term imports Main begin
 
-typedecl cname  --{* class    name *}
-typedecl mname  --{* method   name *}
-typedecl fname  --{* field    name *}
-typedecl vname  --{* variable name *}
+typedecl cname  \<comment>\<open>class    name\<close>
+typedecl mname  \<comment>\<open>method   name\<close>
+typedecl fname  \<comment>\<open>field    name\<close>
+typedecl vname  \<comment>\<open>variable name\<close>
 
 axiomatization
-  This --{* This pointer *}
-  Par  --{* method parameter *}
-  Res  :: vname --{* method result *}
- -- {* Inequality axioms are not required for the meta theory. *}
+  This \<comment>\<open>This pointer\<close>
+  Par  \<comment>\<open>method parameter\<close>
+  Res  :: vname \<comment>\<open>method result\<close>
+ \<comment> \<open>Inequality axioms are not required for the meta theory.\<close>
 (*
 where
   This_neq_Par [simp]: "This \<noteq> Par"
@@ -24,21 +24,21 @@
 *)
 
 datatype stmt
-  = Skip                   --{* empty statement *}
+  = Skip                   \<comment>\<open>empty statement\<close>
   | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
   | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
   | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
-  | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local assignment *}
-  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) --{* field assignment *}
-  | Meth "cname \<times> mname"   --{* virtual method *}
-  | Impl "cname \<times> mname"   --{* method implementation *}
+  | LAss vname expr        ("_ :== _"           [99,   95] 94) \<comment>\<open>local assignment\<close>
+  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) \<comment>\<open>field assignment\<close>
+  | Meth "cname \<times> mname"   \<comment>\<open>virtual method\<close>
+  | Impl "cname \<times> mname"   \<comment>\<open>method implementation\<close>
 and expr
-  = NewC cname       ("new _"        [   99] 95) --{* object creation  *}
-  | Cast cname expr                              --{* type cast        *}
-  | LAcc vname                                   --{* local access     *}
-  | FAcc expr  fname ("_.._"         [95,99] 95) --{* field access     *}
+  = NewC cname       ("new _"        [   99] 95) \<comment>\<open>object creation\<close>
+  | Cast cname expr                              \<comment>\<open>type cast\<close>
+  | LAcc vname                                   \<comment>\<open>local access\<close>
+  | FAcc expr  fname ("_.._"         [95,99] 95) \<comment>\<open>field access\<close>
   | Call cname expr mname expr                   
-                     ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *}
+                     ("{_}_.._'(_')" [99,95,99,95] 95) \<comment>\<open>method call\<close>
 
 end