| changeset 61361 | 8b5f00202e1a |
| parent 58886 | 8a6cac7c7247 |
| child 62042 | 6c6ccf573479 |
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Oct 07 23:28:49 2015 +0200 @@ -4,7 +4,7 @@ *) -section {* JVM Instruction Semantics *} +section \<open>JVM Instruction Semantics\<close> theory JVMExecInstr imports JVMInstructions JVMState begin