src/HOL/UNITY/ROOT.ML
changeset 6012 1894bfc4aee9
parent 5899 13d4753079fe
child 6216 05d99c0bbfa0
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Dec 02 16:14:09 1998 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Thu Dec 03 10:45:06 1998 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4  writeln"Root file for HOL/UNITY";
     1.5  set proof_timing;
     1.6  
     1.7 +
     1.8 +
     1.9  loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    1.10  time_use_thy"UNITY";
    1.11  
    1.12 @@ -27,7 +29,9 @@
    1.13  time_use_thy "Lift";
    1.14  time_use_thy "Comp";
    1.15  time_use_thy "Client";
    1.16 -time_use_thy "PPROD";
    1.17 +(**
    1.18 +time_use_thy "PPX";
    1.19 +**)
    1.20  
    1.21  loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
    1.22  use_thy"NSP_Bad";