# HG changeset patch
# User kleing
# Date 1014905529 -3600
# Node ID 8040cce614e5bca947f28cd10c2d50fe16900cf5
# Parent  da7345ff18e1ac2a90185f2f45824c3dec7b887e
fixed missing label

diff -r da7345ff18e1 -r 8040cce614e5 src/HOL/MicroJava/JVM/JVMListExample.thy
--- 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