--- 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";
--- 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";
--- 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";