changeset 12911 | 704713ca07ea |
parent 12559 | 7fb12775ce98 |
child 12951 | a9fdcb71d252 |
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Feb 21 09:54:08 2002 +0100 @@ -3,7 +3,7 @@ Author: Stefan Berghofer *) -header {* Example for generating executable code from JVM semantics *} +header {* \isaheader{Example for generating executable code from JVM semantics} *} theory JVMListExample = JVMExec: