| changeset 24351 | 1e028d114075 |
| parent 24340 | 811f78424efc |
| child 28520 | 376b9c083b04 |
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 18:11:09 2007 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 20 18:54:51 2007 +0200 @@ -6,7 +6,7 @@ header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} theory BVExample -imports "../JVM/JVMListExample" BVSpecTypeSafe "../JVM/JVM" Executable_Set +imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set begin text {*