src/HOL/MicroJava/ROOT.ML
changeset 12786 d655138ddadf
parent 12773 a47f51daa6dc
child 12911 704713ca07ea
equal deleted inserted replaced
12785:27debaf2112d 12786:d655138ddadf
     2 
     2 
     3 add_path "J";
     3 add_path "J";
     4 add_path "JVM";
     4 add_path "JVM";
     5 add_path "BV";
     5 add_path "BV";
     6 
     6 
     7 use_thy "JVMType"
       
     8 use_thy "JVMExceptions"
       
     9 
       
    10 (*
       
    11 use_thy "JTypeSafe";
     7 use_thy "JTypeSafe";
    12 use_thy "Example";
     8 use_thy "Example";
    13 use_thy "JListExample";
     9 use_thy "JListExample";
    14 use_thy "JVMListExample";
    10 use_thy "JVMListExample";
    15 use_thy "BVSpecTypeSafe";
    11 use_thy "BVSpecTypeSafe";
    16 use_thy "JVM";
    12 use_thy "JVM";
    17 use_thy "LBVSpec"; 
    13 use_thy "LBVSpec"; 
    18 *)
    14 
    19 (* momentarily broken:
    15 (* momentarily broken:
    20 use_thy "LBVCorrect";
    16 use_thy "LBVCorrect";
    21 use_thy "LBVComplete";
    17 use_thy "LBVComplete";
    22 *)
    18 *)