diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -8,32 +8,40 @@
 
 theory Term = Main:
 
-typedecl cname  (* class name *)
-typedecl vnam   (* variable or field name *)
-typedecl mname  (* method name *)
+typedecl cname  --{* class    name *}
+typedecl mname  --{* method   name *}
+typedecl fname  --{* field    name *}
+typedecl vname  --{* variable name *}
 
-datatype vname  (* variable for special names *)
-  = This        (* This pointer *)
-  | Param       (* method parameter *)
-  | Res         (* method result *)
-  | VName vnam 
+consts 
+  This :: vname --{* This pointer *}
+  Par  :: vname --{* method parameter *}
+  Res  :: vname --{* method result *}
+
+text {* Inequality axioms not required here *}
+(*
+axioms
+  This_neq_Par [simp]: "This \<noteq> Par"
+  Par_neq_Res  [simp]: "Par \<noteq> Res"
+  Res_neq_This [simp]: "Res \<noteq> This"
+*)
 
 datatype stmt
-  = Skip                   (* empty statement *)
+  = Skip                   --{* empty statement *}
   | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
   | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
-  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
-  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
-  | Meth "cname \<times> mname"   (* virtual method *)
-  | Impl "cname \<times> mname"   (* method implementation *)
+  | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local ass.*}
+  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) --{* field ass.*}
+  | Meth "cname \<times> mname"   --{* virtual method *}
+  | Impl "cname \<times> mname"   --{* method implementation *}
 and expr
-  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
-  | Cast cname expr                              (* type cast        *)
-  | LAcc vname                                   (* local access     *)
-  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
-  | Call cname expr mname expr                   (* method call      *)
-                     ("{_}_.._'(_')" [99,95,99,95] 95)
+  = NewC cname       ("new _"        [   99] 95) --{* object creation  *}
+  | Cast cname expr                              --{* type cast        *}
+  | LAcc vname                                   --{* local access     *}
+  | FAcc expr  fname ("_.._"         [95,99] 95) --{* field access     *}
+  | Call cname expr mname expr                   
+                     ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *}
 
 end