author | wenzelm |
Mon, 20 Aug 2007 18:54:51 +0200 | |
changeset 24351 | 1e028d114075 |
parent 24350 | 4d74f37c6367 |
child 24352 | eda777a2785b |
--- 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 {*