src/HOL/MicroJava/BV/BVExample.thy
changeset 41413 64cd30d6b0b8
parent 40077 c8a9eaaa2f59
child 44035 322d1657c40c
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -5,7 +5,11 @@
     1.4  header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
     1.5  
     1.6  theory BVExample
     1.7 -imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set
     1.8 +imports
     1.9 +  "../JVM/JVMListExample"
    1.10 +  BVSpecTypeSafe
    1.11 +  JVM
    1.12 +  "~~/src/HOL/Library/Executable_Set"
    1.13  begin
    1.14  
    1.15  text {*