equal
deleted
inserted
replaced
45 x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow> |
45 x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow> |
46 G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)" |
46 G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)" |
47 |
47 |
48 (* cf. 15.7.1 *) |
48 (* cf. 15.7.1 *) |
49 Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s" |
49 Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s" |
|
50 |
|
51 BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1; |
|
52 G\\<turnstile>s1 -e1\\<succ>v2\\<rightarrow> s2; |
|
53 v = (case bop of Eq \\<Rightarrow> Bool (v1 = v2) |
|
54 | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow> |
|
55 G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2" |
50 |
56 |
51 (* cf. 15.13.1, 15.2 *) |
57 (* cf. 15.13.1, 15.2 *) |
52 LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s" |
58 LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s" |
53 |
59 |
54 (* cf. 15.25.1 *) |
60 (* cf. 15.25.1 *) |