equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Effect of instructions on the state type *} |
7 header {* Effect of instructions on the state type *} |
8 |
8 |
9 |
9 |
10 theory Step = Convert: |
10 theory Step = JVMType + JVMExec: |
11 |
11 |
12 |
12 |
13 text "Effect of instruction on the state type:" |
13 text "Effect of instruction on the state type:" |
14 consts |
14 consts |
15 step' :: "instr \<times> jvm_prog \<times> state_type => state_type" |
15 step' :: "instr \<times> jvm_prog \<times> state_type => state_type" |