src/HOL/UNITY/ROOT.ML
changeset 13785 e2fcd88be55d
parent 11193 851c90b23a9e
child 13790 8d7e9fce8c50
equal deleted inserted replaced
13784:b9f6154427a4 13785:e2fcd88be55d
     5 
     5 
     6 Root file for UNITY proofs.
     6 Root file for UNITY proofs.
     7 *)
     7 *)
     8 
     8 
     9 (*Basic meta-theory*)
     9 (*Basic meta-theory*)
    10 time_use_thy "FP";
    10 time_use_thy "UNITY_Main";
    11 time_use_thy "WFair";
       
    12 
    11 
    13 (*Simple examples: no composition*)
    12 (*Simple examples: no composition*)
    14 time_use_thy "Simple/Deadlock";
    13 time_use_thy "Simple/Deadlock";
    15 time_use_thy "Simple/Common";
    14 time_use_thy "Simple/Common";
    16 time_use_thy "Simple/Network";
    15 time_use_thy "Simple/Network";