src/HOL/MicroJava/ROOT.ML
changeset 12441 c586d08520ad
parent 11070 cc421547e744
child 12520 6d754b9a1303
equal deleted inserted replaced
12440:fb5851b71a82 12441:c586d08520ad
     4 add_path "JVM";
     4 add_path "JVM";
     5 add_path "BV";
     5 add_path "BV";
     6 
     6 
     7 use_thy "JTypeSafe";
     7 use_thy "JTypeSafe";
     8 use_thy "Example";
     8 use_thy "Example";
       
     9 use_thy "JListExample";
       
    10 use_thy "JVMListExample";
     9 use_thy "BVSpecTypeSafe";
    11 use_thy "BVSpecTypeSafe";
    10 use_thy "LBVCorrect";
    12 use_thy "LBVCorrect";
    11 use_thy "LBVComplete";
    13 use_thy "LBVComplete";
    12 use_thy "JVM";
    14 use_thy "JVM";