| changeset 61361 | 8b5f00202e1a |
| parent 58886 | 8a6cac7c7247 |
| child 62042 | 6c6ccf573479 |
| 61360:a273bdac0934 | 61361:8b5f00202e1a |
|---|---|
1 (* Title: HOL/MicroJava/JVM/JVMInstructions.thy |
1 (* Title: HOL/MicroJava/JVM/JVMInstructions.thy |
2 Author: Gerwin Klein, Technische Universitaet Muenchen |
2 Author: Gerwin Klein, Technische Universitaet Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* Instructions of the JVM *} |
5 section \<open>Instructions of the JVM\<close> |
6 |
6 |
7 |
7 |
8 theory JVMInstructions imports JVMState begin |
8 theory JVMInstructions imports JVMState begin |
9 |
9 |
10 |
10 |