src/HOL/UNITY/ROOT.ML
changeset 8987 718907f55f62
parent 8334 7896bcbd8641
child 9000 c20d58286a51
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Fri May 26 18:06:43 2000 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri May 26 18:06:58 2000 +0200
     1.3 @@ -23,13 +23,14 @@
     1.4  time_use_thy "Handshake";
     1.5  time_use_thy "Lift";
     1.6  time_use_thy "Comp";
     1.7 +time_use_thy "Reachability";
     1.8  (*Allocator example*)
     1.9 -time_use_thy "Client";
    1.10 -time_use_thy "ELT";  (*obsolete*)
    1.11  time_use_thy "PPROD";
    1.12  time_use_thy "TimerArray";
    1.13 -time_use_thy "Alloc";
    1.14 -time_use_thy "Reachability";
    1.15 +with_path "../Induct" time_use_thy "Alloc";
    1.16 +time_use_thy "Client";
    1.17 +
    1.18 +time_use_thy "ELT";  (*obsolete*)
    1.19  
    1.20  add_path "../Auth";	(*to find Public.thy*)
    1.21  use_thy"NSP_Bad";