added the AllocImpl example
authorpaulson
Fri Jun 23 10:34:51 2000 +0200 (2000-06-23)
changeset 911244fc37919579
parent 9111 33b32680669a
child 9113 e221d4f81d52
added the AllocImpl example
src/HOL/UNITY/ROOT.ML
     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*)