--- 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