--- a/src/HOL/NanoJava/Decl.thy Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/Decl.thy Mon Sep 10 17:35:22 2001 +0200
@@ -9,34 +9,37 @@
theory Decl = Term:
datatype ty
- = NT (* null type *)
- | Class cname (* class type *)
+ = NT --{* null type *}
+ | Class cname --{* class type *}
-types fdecl (* field declaration *)
- = "vnam \<times> ty"
+text{* field declaration *}
+types fdecl
+ = "fname \<times> ty"
-record methd (* method declaration *)
+record methd
= par :: ty
res :: ty
lcl ::"(vname \<times> ty) list"
bdy :: stmt
-types mdecl (* method declaration *)
+text{* method declaration *}
+types mdecl
= "mname \<times> methd"
-record class (* class *)
+record class
= super :: cname
fields ::"fdecl list"
methods ::"mdecl list"
-types cdecl (* class declaration *)
+text{* class declaration *}
+types cdecl
= "cname \<times> class"
types prog
= "cdecl list"
translations
- "fdecl" \<leftharpoondown> (type)"vname \<times> ty"
+ "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
"mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
"class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
"cdecl" \<leftharpoondown> (type)"cname \<times> class"
@@ -44,8 +47,8 @@
consts
- Prog :: prog (* program as a global value *)
- Object :: cname (* name of root class *)
+ Prog :: prog --{* program as a global value *}
+ Object :: cname --{* name of root class *}
constdefs