diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Sun Dec 16 00:18:17 2001 +0100
@@ -8,25 +8,24 @@
 
 theory Term = Value:
 
-datatype binop = Eq | Add    (* function codes for binary operation *)
+datatype binop = Eq | Add    -- "function codes for binary operation"
 
 datatype expr
-  = NewC cname               (* class instance creation *)
-  | Cast cname expr          (* type cast *)
-  | Lit val                  (* literal value, also references *)
-  | BinOp binop expr expr    (* binary operation *)
-  | LAcc vname               (* local (incl. parameter) access *)
-  | LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
-  | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
+  = NewC cname               -- "class instance creation"
+  | Cast cname expr          -- "type cast"
+  | Lit val                  -- "literal value, also references"
+  | BinOp binop expr expr    -- "binary operation"
+  | LAcc vname               -- "local (incl. parameter) access"
+  | LAss vname expr          ("_::=_" [90,90]90)      -- "local assign"
+  | FAcc cname expr vname    ("{_}_.._" [10,90,99]90) -- "field access"
   | FAss cname expr vname 
-                    expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
+                    expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
   | Call cname expr mname 
-    "ty list" "expr list"    (* method call*) ("{_}_.._'( {_}_')"
-                                                            [10,90,99,10,10] 90)
+    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
 
 datatype stmt
-  = Skip                     (* empty statement *)
-  | Expr expr                (* expression statement *)
+  = Skip                     -- "empty statement"
+  | Expr expr                -- "expression statement"
   | Comp stmt stmt       ("_;; _"             [61,60]60)
   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
   | Loop expr stmt       ("While '(_') _"     [80,79]70)