src/HOL/MicroJava/J/JListExample.thy
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 13091 3d12669e599c
--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -1,11 +1,11 @@
-(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
+(*  Title:      HOL/MicroJava/J/JListExample.thy
     ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from Java semantics} *}
 
-theory JListExample = Eval:
+theory JListExample = Eval + SystemClasses:
 
 ML {* Syntax.ambiguity_level := 100000 *}