equal
deleted
inserted
replaced
93 (* cf. 15.8 *) |
93 (* cf. 15.8 *) |
94 NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow> |
94 NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow> |
95 E\\<turnstile>NewC C\\<Colon>Class C" |
95 E\\<turnstile>NewC C\\<Colon>Class C" |
96 |
96 |
97 (* cf. 15.15 *) |
97 (* cf. 15.15 *) |
98 Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>T; |
98 Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>Class C; |
99 prg E\\<turnstile>T\\<preceq>? RefT rt\\<rbrakk> \\<Longrightarrow> |
99 prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow> |
100 E\\<turnstile>Cast rt e\\<Colon>RefT rt" |
100 E\\<turnstile>Cast D e\\<Colon>Class D" |
101 |
101 |
102 (* cf. 15.7.1 *) |
102 (* cf. 15.7.1 *) |
103 Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow> |
103 Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow> |
104 E\\<turnstile>Lit x\\<Colon>T" |
104 E\\<turnstile>Lit x\\<Colon>T" |
105 |
105 |