| changeset 23854 | 688a8a7bcd4e |
| parent 23757 | 087b0a241557 |
| child 24340 | 811f78424efc |
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 19 21:47:39 2007 +0200 @@ -6,7 +6,7 @@ header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} theory BVExample -imports JVMListExample BVSpecTypeSafe JVM ExecutableSet +imports JVMListExample BVSpecTypeSafe JVM Executable_Set begin text {*