equal
deleted
inserted
replaced
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Program Execution in the JVM} *} |
7 header {* \isaheader{Program Execution in the JVM} *} |
8 |
8 |
9 theory JVMExec = JVMExecInstr + JVMExceptions: |
9 theory JVMExec imports JVMExecInstr JVMExceptions begin |
10 |
10 |
11 |
11 |
12 consts |
12 consts |
13 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
13 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
14 |
14 |