changeset 12911 | 704713ca07ea |
parent 12519 | a955fe2879ba |
child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Feb 21 09:54:08 2002 +0100 @@ -4,7 +4,7 @@ Copyright 1999 Technische Universitaet Muenchen *) -header {* Program Execution in the JVM *} +header {* \isaheader{Program Execution in the JVM} *} theory JVMExec = JVMExecInstr + JVMExceptions: