11 consts |
11 consts |
12 subcls1 :: "'c prog => (cname \<times> cname) set" (* subclass *) |
12 subcls1 :: "'c prog => (cname \<times> cname) set" (* subclass *) |
13 widen :: "'c prog => (ty \<times> ty ) set" (* widening *) |
13 widen :: "'c prog => (ty \<times> ty ) set" (* widening *) |
14 cast :: "'c prog => (cname \<times> cname) set" (* casting *) |
14 cast :: "'c prog => (cname \<times> cname) set" (* casting *) |
15 |
15 |
|
16 syntax (xsymbols) |
|
17 subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) |
|
18 subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) |
|
19 widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) |
|
20 cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) |
|
21 |
16 syntax |
22 syntax |
17 subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) |
|
18 subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) |
|
19 widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) |
|
20 cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) |
|
21 |
|
22 syntax (HTML) |
|
23 subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70) |
23 subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70) |
24 subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70) |
24 subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70) |
25 widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70) |
25 widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70) |
26 cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70) |
26 cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70) |
27 |
27 |
28 translations |
28 translations |
29 "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G" |
29 "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G" |
30 "G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*" |
30 "G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*" |
31 "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" |
31 "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" |