equal
deleted
inserted
replaced
5 |
5 |
6 header {* \isaheader{Class Declarations and Programs} *} |
6 header {* \isaheader{Class Declarations and Programs} *} |
7 |
7 |
8 theory Decl imports Type begin |
8 theory Decl imports Type begin |
9 |
9 |
10 types |
10 type_synonym |
11 fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)" |
11 fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)" |
12 |
12 |
|
13 type_synonym |
13 sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2" |
14 sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2" |
14 |
15 |
|
16 type_synonym |
15 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class" |
17 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class" |
16 |
18 |
|
19 type_synonym |
17 'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" |
20 'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" |
18 -- "class = superclass, fields, methods" |
21 -- "class = superclass, fields, methods" |
19 |
22 |
|
23 type_synonym |
20 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1" |
24 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1" |
21 |
25 |
|
26 type_synonym |
22 'c prog = "'c cdecl list" -- "program" |
27 'c prog = "'c cdecl list" -- "program" |
23 |
28 |
24 |
29 |
25 translations |
30 translations |
26 (type) "fdecl" <= (type) "vname \<times> ty" |
31 (type) "fdecl" <= (type) "vname \<times> ty" |