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