add_path / reset_path;
authorwenzelm
Wed Feb 03 17:34:27 1999 +0100 (1999-02-03)
changeset 621605d99c0bbfa0
parent 6215 6165747678ba
child 6217 9dac1ee185e3
add_path / reset_path;
src/HOL/Lambda/ROOT.ML
src/HOL/UNITY/NSP_Bad.thy
src/HOL/UNITY/ROOT.ML
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Wed Feb 03 17:33:41 1999 +0100
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     1.3 @@ -9,5 +9,5 @@
     1.4  writeln"Root file for HOL/Lambda";
     1.5  
     1.6  time_use_thy "Eta";
     1.7 -loadpath := [".","../Induct"];
     1.8 +add_path "../Induct";
     1.9  time_use_thy "InductTermi";
     2.1 --- a/src/HOL/UNITY/NSP_Bad.thy	Wed Feb 03 17:33:41 1999 +0100
     2.2 +++ b/src/HOL/UNITY/NSP_Bad.thy	Wed Feb 03 17:34:27 1999 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1996  University of Cambridge
     2.6  
     2.7 -loadpath := "../Auth" :: !loadpath; use_thy"NSP_Bad";
     2.8 +add_path "../Auth"; use_thy"NSP_Bad";
     2.9  
    2.10  Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
    2.11  
     3.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Feb 03 17:33:41 1999 +0100
     3.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     3.3 @@ -11,9 +11,8 @@
     3.4  writeln"Root file for HOL/UNITY";
     3.5  set proof_timing;
     3.6  
     3.7 -
     3.8 +add_path "../Lex";	(*to find Prefix.thy*)
     3.9  
    3.10 -loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    3.11  time_use_thy"UNITY";
    3.12  
    3.13  time_use_thy "Deadlock";
    3.14 @@ -33,5 +32,7 @@
    3.15  time_use_thy "PPX";
    3.16  **)
    3.17  
    3.18 -loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
    3.19 +add_path "../Auth";	(*to find Public.thy*)
    3.20  use_thy"NSP_Bad";
    3.21 +
    3.22 +reset_path ();