| changeset 10591 | 6d6cb845e841 |
| parent 10057 | 8c8d2d0d3ef8 |
| child 10897 | 697fab84709e |
| 10590:315afa77adea | 10591:6d6cb845e841 |
|---|---|
31 | Ifcmpeq int (* Branch if int/ref comparison succeeds *) |
31 | Ifcmpeq int (* Branch if int/ref comparison succeeds *) |
32 |
32 |
33 |
33 |
34 types |
34 types |
35 bytecode = "instr list" |
35 bytecode = "instr list" |
36 jvm_prog = "(nat \<times> bytecode) prog" |
36 jvm_prog = "(nat \<times> nat \<times> bytecode) prog" |
37 |
37 |
38 end |
38 end |