src/HOL/UNITY/ROOT.ML
changeset 6299 1a88db6e7c7e
parent 6295 351b3c2b0d83
child 6349 f7750d816c21
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:36:24 1999 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:50:42 1999 +0100
     1.3 @@ -28,10 +28,8 @@
     1.4  time_use_thy "Lift";
     1.5  time_use_thy "Comp";
     1.6  time_use_thy "Client";
     1.7 -(**
     1.8  time_use_thy "Extend";
     1.9  time_use_thy "PPROD";
    1.10 -**)
    1.11  
    1.12  add_path "../Auth";	(*to find Public.thy*)
    1.13  use_thy"NSP_Bad";