changeset 58886 | 8a6cac7c7247 |
parent 39758 | b8a53e3a0ee2 |
child 61361 | 8b5f00202e1a |
58885:47fdd4f40d00 | 58886:8a6cac7c7247 |
---|---|
2 Author: Cornelia Pusch, Gerwin Klein |
2 Author: Cornelia Pusch, Gerwin Klein |
3 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 |
6 |
7 header {* \isaheader{JVM Instruction Semantics} *} |
7 section {* JVM Instruction Semantics *} |
8 |
8 |
9 |
9 |
10 theory JVMExecInstr imports JVMInstructions JVMState begin |
10 theory JVMExecInstr imports JVMInstructions JVMState begin |
11 |
11 |
12 |
12 |