--- a/src/HOLCF/IMP/ROOT.ML Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IMP/ROOT.ML Wed Feb 03 17:36:55 1999 +0100
@@ -4,15 +4,8 @@
Copyright 1997 TU Muenchen
*)
-(*Load theories from ../meta_theory without generating HTML files
- (has already been done by HOL/IMP/ROOT.ML)*)
-val old_make_html = !make_html;
-make_html := false;
-loadpath := ["../../HOL/IMP"];
-
+add_path "../../HOL/IMP";
use_thy "Natural";
-make_html := old_make_html;
-loadpath := ["."];
-
+reset_path ();
use_thy "HoareEx";
--- a/src/HOLCF/IOA/ABP/ROOT.ML Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Wed Feb 03 17:36:55 1999 +0100
@@ -9,6 +9,4 @@
goals_limit := 1;
-loadpath:=["."];
-
use_thy "Correctness";
--- a/src/HOLCF/IOA/NTP/ROOT.ML Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML Wed Feb 03 17:36:55 1999 +0100
@@ -9,6 +9,4 @@
goals_limit := 1;
-loadpath:=["."];
-
use_thy "Correctness";
--- a/src/HOLCF/IOA/ROOT.ML Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/ROOT.ML Wed Feb 03 17:36:55 1999 +0100
@@ -3,18 +3,16 @@
Author: Olaf Mueller
Copyright 1997 TU Muenchen
-This is the ROOT file for the formalization of a semantic model of I/O-Automata.
-
-See the README.html file for details.
-
-Should be executed in the subdirectory HOLCF/IOA/meta_theory.
+This is the ROOT file for the formalization of a semantic model of
+I/O-Automata. See the README.html file for details.
*)
+goals_limit := 1;
-goals_limit:=1;
+add_path "meta_theory";
-loadpath := ["meta_theory"];
+use_thy "Abstraction";
+use_thy "TrivEx";
+use_thy "TrivEx2";
-use_thy"Abstraction";
-use_thy"TrivEx";
-use_thy"TrivEx2";
\ No newline at end of file
+reset_path ();
--- a/src/HOLCF/IOA/Storage/ROOT.ML Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/Storage/ROOT.ML Wed Feb 03 17:36:55 1999 +0100
@@ -8,6 +8,4 @@
goals_limit := 1;
-loadpath:=["."];
-
use_thy "Correctness";