changeset 12911 | 704713ca07ea |
parent 12519 | a955fe2879ba |
child 13677 | 5fad004bd9df |
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Feb 21 09:54:08 2002 +0100 @@ -5,7 +5,7 @@ *) -header {* JVM Instruction Semantics *} +header {* \isaheader{JVM Instruction Semantics} *} theory JVMExecInstr = JVMInstructions + JVMState: