equal
deleted
inserted
replaced
6 header {* \isaheader{Effect of Instructions on the State Type} *} |
6 header {* \isaheader{Effect of Instructions on the State Type} *} |
7 |
7 |
8 theory Effect |
8 theory Effect |
9 imports JVMType "../JVM/JVMExceptions" |
9 imports JVMType "../JVM/JVMExceptions" |
10 begin |
10 begin |
11 |
|
12 |
11 |
13 types |
12 types |
14 succ_type = "(p_count \<times> state_type option) list" |
13 succ_type = "(p_count \<times> state_type option) list" |
15 |
14 |
16 text {* Program counter of successor instructions: *} |
15 text {* Program counter of successor instructions: *} |