src/HOL/UNITY/ROOT.ML
changeset 6216 05d99c0bbfa0
parent 6012 1894bfc4aee9
child 6295 351b3c2b0d83
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Feb 03 17:33:41 1999 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     1.3 @@ -11,9 +11,8 @@
     1.4  writeln"Root file for HOL/UNITY";
     1.5  set proof_timing;
     1.6  
     1.7 -
     1.8 +add_path "../Lex";	(*to find Prefix.thy*)
     1.9  
    1.10 -loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    1.11  time_use_thy"UNITY";
    1.12  
    1.13  time_use_thy "Deadlock";
    1.14 @@ -33,5 +32,7 @@
    1.15  time_use_thy "PPX";
    1.16  **)
    1.17  
    1.18 -loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
    1.19 +add_path "../Auth";	(*to find Public.thy*)
    1.20  use_thy"NSP_Bad";
    1.21 +
    1.22 +reset_path ();