--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Feb 28 13:38:49 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Feb 28 15:12:09 2002 +0100
@@ -3,7 +3,7 @@
Author: Stefan Berghofer
*)
-header {* \isaheader{Example for generating executable code from JVM semantics} *}
+header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
theory JVMListExample = SystemClasses + JVMExec:
@@ -187,4 +187,4 @@
ML {* exec (E, the it) *}
ML {* exec (E, the it) *}
-end
\ No newline at end of file
+end