src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 12973 8040cce614e5
parent 12951 a9fdcb71d252
child 13052 3bf41c474a88
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Feb 28 13:38:49 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Feb 28 15:12:09 2002 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Stefan Berghofer
     1.5  *)
     1.6  
     1.7 -header {* \isaheader{Example for generating executable code from JVM semantics} *}
     1.8 +header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
     1.9  
    1.10  theory JVMListExample = SystemClasses + JVMExec:
    1.11  
    1.12 @@ -187,4 +187,4 @@
    1.13  ML {* exec (E, the it) *}
    1.14  ML {* exec (E, the it) *}
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end