9 theory TypeRel imports Decl begin |
9 theory TypeRel imports Decl begin |
10 |
10 |
11 consts |
11 consts |
12 subcls1 :: "(cname \<times> cname) set" --{* subclass *} |
12 subcls1 :: "(cname \<times> cname) set" --{* subclass *} |
13 |
13 |
14 syntax (xsymbols) |
14 abbreviation |
15 subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70) |
15 subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) |
16 subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70) |
16 where "C <=C1 D == (C,D) \<in> subcls1" |
17 syntax |
17 abbreviation |
18 subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) |
18 subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) |
19 subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) |
19 where "C <=C D == (C,D) \<in> subcls1^*" |
20 |
20 |
21 translations |
21 notation (xsymbols) |
22 "C \<prec>C1 D" == "(C,D) \<in> subcls1" |
22 subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and |
23 "C \<preceq>C D" == "(C,D) \<in> subcls1^*" |
23 subcls_syntax ("_ \<preceq>C _" [71,71] 70) |
24 |
24 |
25 consts |
25 consts |
26 method :: "cname => (mname \<rightharpoonup> methd)" |
26 method :: "cname => (mname \<rightharpoonup> methd)" |
27 field :: "cname => (fname \<rightharpoonup> ty)" |
27 field :: "cname => (fname \<rightharpoonup> ty)" |
28 |
28 |