| changeset 16417 | 9bc16273c2d4 |
| parent 15570 | 8d8c70b41bab |
| child 16643 | 39cb9fe20fe3 |
--- a/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 17 16:12:49 2005 +0200 @@ -5,7 +5,7 @@ header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} -theory BVExample = JVMListExample + BVSpecTypeSafe + JVM: +theory BVExample imports JVMListExample BVSpecTypeSafe JVM begin text {* This theory shows type correctness of the example program in section