more graceful handling of load paths;
authorwenzelm
Thu Apr 22 18:20:37 1999 +0200 (1999-04-22)
changeset 6488271969bb7f95
parent 6487 453901eb3412
child 6489 e02c5290885d
more graceful handling of load paths;
src/HOLCF/IMP/ROOT.ML
src/HOLCF/IOA/Modelcheck/ROOT.ML
src/HOLCF/IOA/ROOT.ML
     1.1 --- a/src/HOLCF/IMP/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
     1.2 +++ b/src/HOLCF/IMP/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
     1.3 @@ -4,8 +4,5 @@
     1.4      Copyright   1997  TU Muenchen
     1.5  *)
     1.6  
     1.7 -add_path "../../HOL/IMP";
     1.8 -use_thy "Natural";
     1.9 -
    1.10 -reset_path ();
    1.11 +use_thy "../../HOL/IMP/Natural";
    1.12  use_thy "HoareEx";
     2.1 --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
     2.2 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/IOA/Modelcheck/ROOT.ML
     2.5 +(*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
     2.6      ID:         $Id$
     2.7      Author:     Olaf Mueller
     2.8      Copyright   1997  TU Muenchen
     2.9 @@ -9,10 +9,8 @@
    2.10  
    2.11  goals_limit := 1;
    2.12  
    2.13 -add_path"~/isabelle/src/HOL/Modelcheck";
    2.14 -use"~/isabelle/src/HOL/Modelcheck/mucke_oracle.ML";
    2.15 -use_thy"MuIOAOracle";
    2.16 -use_thy"Cockpit";
    2.17 -use_thy"Ring3";
    2.18 -
    2.19 -reset_path();
    2.20 +use "../../../HOL/Modelcheck/mucke_oracle.ML";
    2.21 +use_thy "../../../HOL/Modelcheck/MuckeSyn";
    2.22 +use_thy "MuIOAOracle";
    2.23 +use_thy "Cockpit";
    2.24 +use_thy "Ring3";
     3.1 --- a/src/HOLCF/IOA/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
     3.2 +++ b/src/HOLCF/IOA/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/IOA/meta_theory/ROOT.ML
     3.5 +(*  Title:      HOL/IOA/ROOT.ML
     3.6      ID:         $Id$
     3.7      Author:     Olaf Mueller
     3.8      Copyright   1997  TU Muenchen
     3.9 @@ -9,9 +9,6 @@
    3.10  
    3.11  goals_limit := 1;
    3.12  
    3.13 -add_path "meta_theory";
    3.14 -
    3.15 -use_thy "Abstraction";
    3.16 -
    3.17 -use"~/isabelle/src/HOLCF/IOA/meta_theory/ioa_package.ML";
    3.18 -use"~/isabelle/src/HOLCF/IOA/meta_theory/ioa_syn.ML";
    3.19 +use_thy "meta_theory/Abstraction";
    3.20 +use "meta_theory/ioa_package.ML";
    3.21 +use "meta_theory/ioa_syn.ML";