src/HOL/MicroJava/J/Term.thy

--- a/src/HOL/MicroJava/J/Term.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -14,21 +14,21 @@
   | Lit val                  \<comment> \<open>literal value, also references\<close>
   | BinOp binop expr expr    \<comment> \<open>binary operation\<close>
   | LAcc vname               \<comment> \<open>local (incl. parameter) access\<close>
-  | LAss vname expr          ("_::=_" [90,90]90)      \<comment> \<open>local assign\<close>
-  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) \<comment> \<open>field access\<close>
+  | LAss vname expr          (\<open>_::=_\<close> [90,90]90)      \<comment> \<open>local assign\<close>
+  | FAcc cname expr vname    (\<open>{_}_.._\<close> [10,90,99]90) \<comment> \<open>field access\<close>
   | FAss cname expr vname 
-                    expr     ("{_}_.._:=_" [10,90,99,90]90) \<comment> \<open>field ass.\<close>
+                    expr     (\<open>{_}_.._:=_\<close> [10,90,99,90]90) \<comment> \<open>field ass.\<close>
   | Call cname expr mname 
-    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) \<comment> \<open>method call\<close>
+    "ty list" "expr list"    (\<open>{_}_.._'( {_}_')\<close> [10,90,99,10,10] 90) \<comment> \<open>method call\<close>
 
 datatype_compat expr
 
 datatype stmt
   = Skip                     \<comment> \<open>empty statement\<close>
   | Expr expr                \<comment> \<open>expression statement\<close>
-  | Comp stmt stmt       ("_;; _"             [61,60]60)
-  | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
-  | Loop expr stmt       ("While '(_') _"     [80,79]70)
+  | Comp stmt stmt       (\<open>_;; _\<close>             [61,60]60)
+  | Cond expr stmt stmt  (\<open>If '(_') _ Else _\<close> [80,79,79]70)
+  | Loop expr stmt       (\<open>While '(_') _\<close>     [80,79]70)
 
 end