| changeset 11177 | 749fd046002f |
| parent 10922 | f1209aff9517 |
| child 12519 | a955fe2879ba |
| 11176:dec03152d163 | 11177:749fd046002f |
|---|---|
38 |
38 |
39 text {* runtime state: *} |
39 text {* runtime state: *} |
40 types |
40 types |
41 jvm_state = "xcpt option \<times> aheap \<times> frame list" |
41 jvm_state = "xcpt option \<times> aheap \<times> frame list" |
42 |
42 |
43 |
|
44 text {* dynamic method lookup: *} |
|
45 constdefs |
|
46 dyn_class :: "'code prog \<times> sig \<times> cname => cname" |
|
47 "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
|
48 |
|
49 end |
43 end |