tidied load path handling;
authorwenzelm
Wed Feb 03 17:36:55 1999 +0100 (1999-02-03)
changeset 62179dac1ee185e3
parent 6216 05d99c0bbfa0
child 6218 3e9d6edc99a8
tidied load path handling;
src/HOLCF/IMP/ROOT.ML
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/Storage/ROOT.ML
     1.1 --- a/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     1.2 +++ b/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     1.3 @@ -4,15 +4,8 @@
     1.4      Copyright   1997  TU Muenchen
     1.5  *)
     1.6  
     1.7 -(*Load theories from ../meta_theory without generating HTML files
     1.8 -  (has already been done by HOL/IMP/ROOT.ML)*)
     1.9 -val old_make_html = !make_html;
    1.10 -make_html := false;
    1.11 -loadpath := ["../../HOL/IMP"];
    1.12 -
    1.13 +add_path "../../HOL/IMP";
    1.14  use_thy "Natural";
    1.15  
    1.16 -make_html := old_make_html;
    1.17 -loadpath := ["."];
    1.18 -
    1.19 +reset_path ();
    1.20  use_thy "HoareEx";
     2.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     2.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     2.3 @@ -9,6 +9,4 @@
     2.4  
     2.5  goals_limit := 1;
     2.6  
     2.7 -loadpath:=["."];
     2.8 -
     2.9  use_thy "Correctness";
     3.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     3.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     3.3 @@ -9,6 +9,4 @@
     3.4  
     3.5  goals_limit := 1;
     3.6  
     3.7 -loadpath:=["."];
     3.8 -
     3.9  use_thy "Correctness";
     4.1 --- a/src/HOLCF/IOA/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     4.2 +++ b/src/HOLCF/IOA/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     4.3 @@ -3,18 +3,16 @@
     4.4      Author:     Olaf Mueller
     4.5      Copyright   1997  TU Muenchen
     4.6  
     4.7 -This is the ROOT file for the formalization of a semantic model of I/O-Automata.
     4.8 -
     4.9 -See the README.html file for details.
    4.10 -
    4.11 -Should be executed in the subdirectory HOLCF/IOA/meta_theory.
    4.12 +This is the ROOT file for the formalization of a semantic model of
    4.13 +I/O-Automata.  See the README.html file for details.
    4.14  *)
    4.15  
    4.16 +goals_limit := 1;
    4.17  
    4.18 -goals_limit:=1;
    4.19 +add_path "meta_theory";
    4.20  
    4.21 -loadpath := ["meta_theory"];
    4.22 +use_thy "Abstraction";
    4.23 +use_thy "TrivEx";
    4.24 +use_thy "TrivEx2";
    4.25  
    4.26 -use_thy"Abstraction";
    4.27 -use_thy"TrivEx";
    4.28 -use_thy"TrivEx2";
    4.29 \ No newline at end of file
    4.30 +reset_path ();
     5.1 --- a/src/HOLCF/IOA/Storage/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     5.2 +++ b/src/HOLCF/IOA/Storage/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     5.3 @@ -8,6 +8,4 @@
     5.4  
     5.5  goals_limit := 1;
     5.6  
     5.7 -loadpath:=["."];
     5.8 -
     5.9  use_thy "Correctness";