changeset 12911 | 704713ca07ea |
parent 12519 | a955fe2879ba |
child 13674 | f4c64597fb02 |
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Thu Feb 21 09:54:08 2002 +0100 @@ -4,7 +4,7 @@ Copyright 2000 Technische Universitaet Muenchen *) -header {* Instructions of the JVM *} +header {* \isaheader{Instructions of the JVM} *} theory JVMInstructions = JVMState: