src/HOL/UNITY/ROOT.ML
changeset 8314 463f63a9a7f2
parent 8251 9be357df93d4
child 8334 7896bcbd8641
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Tue Feb 29 10:41:08 2000 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Tue Feb 29 10:57:30 2000 +0100
     1.3 @@ -28,9 +28,7 @@
     1.4  time_use_thy "Extend";
     1.5  time_use_thy "PPROD";
     1.6  time_use_thy "TimerArray";
     1.7 -(**
     1.8  time_use_thy "Alloc";
     1.9 -**)
    1.10  
    1.11  add_path "../Auth";	(*to find Public.thy*)
    1.12  use_thy"NSP_Bad";