equal
deleted
inserted
replaced
19 widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70) |
19 widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70) |
20 cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70) |
20 cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70) |
21 |
21 |
22 translations |
22 translations |
23 "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
23 "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
24 "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^+" |
24 "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^*" |
25 "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
25 "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
26 "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G" |
26 "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G" |
27 |
27 |
28 defs |
28 defs |
29 |
29 |