src/HOL/UNITY/ROOT.ML
changeset 11193 851c90b23a9e
parent 10782 ddb433987557
child 13785 e2fcd88be55d
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Mar 05 12:31:31 2001 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Mon Mar 05 15:25:11 2001 +0100
     1.3 @@ -6,35 +6,39 @@
     1.4  Root file for UNITY proofs.
     1.5  *)
     1.6  
     1.7 -time_use_thy "UNITY";
     1.8 -time_use_thy "Deadlock";
     1.9 +(*Basic meta-theory*)
    1.10 +time_use_thy "FP";
    1.11  time_use_thy "WFair";
    1.12 -time_use_thy "Common";
    1.13 -time_use_thy "Network";
    1.14 -time_use_thy "Token";
    1.15 -time_use_thy "Channel";
    1.16 -time_use_thy "Mutex";
    1.17 -time_use_thy "FP";
    1.18 -time_use_thy "Reach";
    1.19 -time_use_thy "Handshake";
    1.20 -time_use_thy "Lift";
    1.21 +
    1.22 +(*Simple examples: no composition*)
    1.23 +time_use_thy "Simple/Deadlock";
    1.24 +time_use_thy "Simple/Common";
    1.25 +time_use_thy "Simple/Network";
    1.26 +time_use_thy "Simple/Token";
    1.27 +time_use_thy "Simple/Channel";
    1.28 +time_use_thy "Simple/Lift";
    1.29 +time_use_thy "Simple/Mutex";
    1.30 +time_use_thy "Simple/Reach";
    1.31 +time_use_thy "Simple/Reachability";
    1.32 +
    1.33 +with_path "../Auth"  (*to find Public.thy*)
    1.34 +  time_use_thy"Simple/NSP_Bad";
    1.35 +
    1.36 +(*Example of composition*)
    1.37  time_use_thy "Comp";
    1.38 -time_use_thy "Reachability";
    1.39 +time_use_thy "Comp/Handshake";
    1.40  
    1.41  (*Universal properties examples*)
    1.42 -time_use_thy "Counter";
    1.43 -time_use_thy "Counterc";
    1.44 -time_use_thy "Priority";
    1.45 +time_use_thy "Comp/Counter";
    1.46 +time_use_thy "Comp/Counterc";
    1.47 +time_use_thy "Comp/Priority";
    1.48  
    1.49  (*Allocator example*)
    1.50  time_use_thy "PPROD";
    1.51 -time_use_thy "TimerArray";
    1.52 +time_use_thy "Comp/TimerArray";
    1.53  
    1.54 -time_use_thy "Alloc";
    1.55 -time_use_thy "AllocImpl";
    1.56 -time_use_thy "Client";
    1.57 +time_use_thy "Comp/Alloc";
    1.58 +time_use_thy "Comp/AllocImpl";
    1.59 +time_use_thy "Comp/Client";
    1.60  
    1.61  time_use_thy "ELT";  (*obsolete*)
    1.62 -
    1.63 -with_path "../Auth"  (*to find Public.thy*)
    1.64 -  time_use_thy"NSP_Bad";