--- a/src/HOL/MicroJava/J/Decl.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Sat Apr 23 13:00:19 2011 +0200
@@ -7,18 +7,23 @@
theory Decl imports Type begin
-types
+type_synonym
fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
+type_synonym
sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2"
+type_synonym
'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
+type_synonym
'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list"
-- "class = superclass, fields, methods"
+type_synonym
'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
+type_synonym
'c prog = "'c cdecl list" -- "program"