| changeset 24340 | 811f78424efc |
| parent 23854 | 688a8a7bcd4e |
| child 24351 | 1e028d114075 |
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 17:34:04 2007 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 17:46:31 2007 +0200 @@ -6,7 +6,7 @@ header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} theory BVExample -imports JVMListExample BVSpecTypeSafe JVM Executable_Set +imports "../JVM/JVMListExample" BVSpecTypeSafe "../JVM/JVM" Executable_Set begin text {*