src/HOL/UNITY/ROOT.ML
changeset 6295 351b3c2b0d83
parent 6216 05d99c0bbfa0
child 6299 1a88db6e7c7e
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Mar 01 18:37:52 1999 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Mon Mar 01 18:38:43 1999 +0100
     1.3 @@ -29,7 +29,8 @@
     1.4  time_use_thy "Comp";
     1.5  time_use_thy "Client";
     1.6  (**
     1.7 -time_use_thy "PPX";
     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*)