src/HOL/UNITY/ROOT.ML
changeset 9112 44fc37919579
parent 9000 c20d58286a51
child 10265 4e004b548049
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Fri Jun 23 10:34:31 2000 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Jun 23 10:34:51 2000 +0200
     1.3 @@ -20,10 +20,14 @@
     1.4  time_use_thy "Lift";
     1.5  time_use_thy "Comp";
     1.6  time_use_thy "Reachability";
     1.7 +
     1.8  (*Allocator example*)
     1.9  time_use_thy "PPROD";
    1.10  time_use_thy "TimerArray";
    1.11 -with_path "../Induct" time_use_thy "Alloc";
    1.12 +
    1.13 +add_path "../Induct";
    1.14 +time_use_thy "Alloc";
    1.15 +time_use_thy "AllocImpl";
    1.16  time_use_thy "Client";
    1.17  
    1.18  time_use_thy "ELT";  (*obsolete*)