| 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: