# HG changeset patch
# User wenzelm
# Date 924798037 -7200
# Node ID 271969bb7f95ae6cbf93deaf005c3f2ec2bbf72a
# Parent  453901eb34124f57630a75643182f0d23a759c52
more graceful handling of load paths;

diff -r 453901eb3412 -r 271969bb7f95 src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
@@ -4,8 +4,5 @@
     Copyright   1997  TU Muenchen
 *)
 
-add_path "../../HOL/IMP";
-use_thy "Natural";
-
-reset_path ();
+use_thy "../../HOL/IMP/Natural";
 use_thy "HoareEx";
diff -r 453901eb3412 -r 271969bb7f95 src/HOLCF/IOA/Modelcheck/ROOT.ML
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/Modelcheck/ROOT.ML
+(*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1997  TU Muenchen
@@ -9,10 +9,8 @@
 
 goals_limit := 1;
 
-add_path"~/isabelle/src/HOL/Modelcheck";
-use"~/isabelle/src/HOL/Modelcheck/mucke_oracle.ML";
-use_thy"MuIOAOracle";
-use_thy"Cockpit";
-use_thy"Ring3";
-
-reset_path();
+use "../../../HOL/Modelcheck/mucke_oracle.ML";
+use_thy "../../../HOL/Modelcheck/MuckeSyn";
+use_thy "MuIOAOracle";
+use_thy "Cockpit";
+use_thy "Ring3";
diff -r 453901eb3412 -r 271969bb7f95 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Thu Apr 22 18:18:47 1999 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Thu Apr 22 18:20:37 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/meta_theory/ROOT.ML
+(*  Title:      HOL/IOA/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1997  TU Muenchen
@@ -9,9 +9,6 @@
 
 goals_limit := 1;
 
-add_path "meta_theory";
-
-use_thy "Abstraction";
-
-use"~/isabelle/src/HOLCF/IOA/meta_theory/ioa_package.ML";
-use"~/isabelle/src/HOLCF/IOA/meta_theory/ioa_syn.ML";
+use_thy "meta_theory/Abstraction";
+use "meta_theory/ioa_package.ML";
+use "meta_theory/ioa_syn.ML";