| changeset 24340 | 811f78424efc |
| parent 24225 | 348e982c694b |
| child 24783 | 5a3e336a2e37 |
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 20 17:34:04 2007 +0200 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 20 17:46:31 2007 +0200 @@ -5,7 +5,7 @@ header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *} -theory JVMListExample imports SystemClasses JVMExec begin +theory JVMListExample imports "../J/SystemClasses" JVMExec begin consts list_nam :: cnam