# HG changeset patch
# User clasohm
# Date 816954189 -3600
# Node ID 4a960c01238398b9015ee94a31333878090fca66
# Parent  5bf4a54ba25f215cc792fe03f987c7c85c58b729
removed make_chart;
theories are now read from the current directory (because of use_dir)

diff -r 5bf4a54ba25f -r 4a960c012383 src/CCL/ex/ROOT.ML
--- a/src/CCL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/CCL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -10,13 +10,11 @@
 
 writeln"Root file for CCL examples";
 proof_timing := true;
-loadpath := [".", "ex"];
 
-time_use_thy "ex/Nat";
-time_use_thy "ex/List";
-time_use_thy "ex/Stream";
-time_use_thy "ex/Flag";
+time_use_thy "Nat";
+time_use_thy "List";
+time_use_thy "Stream";
+time_use_thy "Flag";
 
-make_chart ();   (*make HTML chart*)
-
+cd "..";
 maketest"END: Root file for CCL examples";
diff -r 5bf4a54ba25f -r 4a960c012383 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/FOL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -12,31 +12,30 @@
 
 proof_timing := true;
 
-time_use     "ex/intro.ML";
-time_use_thy "ex/Nat";
-time_use     "ex/foundn.ML";
-time_use_thy "ex/Prolog";
+time_use     "intro.ML";
+time_use_thy "Nat";
+time_use     "foundn.ML";
+time_use_thy "Prolog";
 
 writeln"\n** Intuitionistic examples **\n";
-time_use     "ex/int.ML";
+time_use     "int.ML";
 
 val thy = IFOL.thy  and  tac = Int.fast_tac 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 
 writeln"\n** Classical examples **\n";
-time_use     "ex/mini.ML";
-time_use     "ex/cla.ML";
-time_use_thy "ex/If";
+time_use     "mini.ML";
+time_use     "cla.ML";
+time_use_thy "If";
 
 val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 
 writeln"\n** Simplification examples **\n";
-time_use_thy "ex/Nat2";
-time_use_thy "ex/List";
+time_use_thy "Nat2";
+time_use_thy "List";
 
-make_chart ();   (*make HTML chart*)
-
+cd "..";
 maketest"END: Root file for FOL examples";
diff -r 5bf4a54ba25f -r 4a960c012383 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -12,26 +12,25 @@
 
 proof_timing := true;
 
-time_use     "ex/intro.ML";
-time_use_thy "ex/Nat";
-time_use     "ex/foundn.ML";
+time_use     "intro.ML";
+time_use_thy "Nat";
+time_use     "foundn.ML";
 
 writeln"\n** Intuitionistic examples **\n";
-time_use     "ex/int.ML";
+time_use     "int.ML";
 
 val thy = IFOLP.thy  and  tac = Int.fast_tac 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 commit();
 
 writeln"\n** Classical examples **\n";
-time_use     "ex/cla.ML";
-time_use_thy "ex/If";
+time_use     "cla.ML";
+time_use_thy "If";
 
 val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 
-make_chart ();   (*make HTML chart*)
-
+cd "..";
 maketest"END: Root file for FOLP examples";
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/Hoare/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -6,7 +6,4 @@
 
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
-loadpath := ["Hoare"];
 use_thy "Examples";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/IMP/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -8,9 +8,6 @@
 
 writeln"Root file for HOL/IMP";
 proof_timing := true;
-loadpath := [".","IMP"];
 time_use_thy "Properties";
 time_use_thy "Equiv";
 time_use_thy "Hoare";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/Integ/ROOT.ML
--- a/src/HOL/Integ/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/Integ/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -8,7 +8,4 @@
 
 HOL_build_completed;    (*Cause examples to fail if HOL did*)
 
-loadpath := ["Integ"];
 time_use_thy "Integ";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -7,8 +7,5 @@
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/Lambda";
-loadpath := [".","Lambda"];
 
 time_use_thy "Eta";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/Lex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -6,8 +6,4 @@
 
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
-loadpath := ["Lex"];
-
 use_thy"AutoChopper";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -9,9 +9,6 @@
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/MiniML";
-loadpath := [".","MiniML"];
 Unify.trace_bound := 20;
 
 time_use_thy "I";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/Subst/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -26,10 +26,7 @@
 HOL_build_completed;    (*Cause examples to fail if HOL did*)
 
 writeln"Root file for Substitutions and Unification";
-loadpath := ["Subst"];
 
 use_thy "Unifier";
 
-make_chart ();   (*make HTML chart*)
-
 writeln"END: Root file for Substitutions and Unification";
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -10,10 +10,9 @@
 
 writeln "Root file for HOL examples";
 proof_timing := true;
-loadpath := ["ex"];
-time_use     "ex/cla.ML";
-time_use     "ex/meson.ML";
-time_use     "ex/mesontest.ML";
+time_use     "cla.ML";
+time_use     "meson.ML";
+time_use     "mesontest.ML";
 time_use_thy "String";
 time_use_thy "BT";
 time_use_thy "Perm";
@@ -22,7 +21,7 @@
 time_use_thy "LexProd";
 time_use_thy "Puzzle";
 time_use_thy "NatSum";
-time_use     "ex/set.ML";
+time_use     "set.ML";
 time_use_thy "SList";
 time_use_thy "LList";
 time_use_thy "Acc";
@@ -31,6 +30,4 @@
 time_use_thy "Simult";
 time_use_thy "MT";
 
-make_chart ();   (*make HTML chart*)
-
 writeln "END: Root file for HOL examples";
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOLCF/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -10,11 +10,11 @@
 
 writeln"Root file for HOLCF examples";
 proof_timing := true;
-time_use_thy "ex/Hoare";
-time_use_thy "ex/Loop";
-time_use_thy "ex/Fix2";
-time_use "ex/loeckx.ML";
 
-make_chart ();   (*make HTML chart*)
+time_use_thy "Hoare";
+time_use_thy "Loop";
+time_use_thy "Fix2";
+time_use "loeckx.ML";
 
+cd "..";
 maketest     "END: Root file for HOLCF examples";
diff -r 5bf4a54ba25f -r 4a960c012383 src/HOLCF/explicit_domains/ROOT.ML
--- a/src/HOLCF/explicit_domains/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOLCF/explicit_domains/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -9,14 +9,16 @@
 
 writeln"Root file for HOLCF examples: explicit domain axiomatisation";
 proof_timing := true;
-time_use_thy "explicit_domains/Dnat";
-time_use_thy "explicit_domains/Dnat2";
-time_use_thy "explicit_domains/Stream";
-time_use_thy "explicit_domains/Stream2";
-time_use_thy "explicit_domains/Dlist";
+
+time_use_thy "Dnat";
+time_use_thy "Dnat2";
+time_use_thy "Stream";
+time_use_thy "Stream2";
+time_use_thy "Dlist";
 
-time_use_thy "explicit_domains/Coind";
-time_use_thy "explicit_domains/Dagstuhl";
-time_use_thy "explicit_domains/Focus_ex";
+time_use_thy "Coind";
+time_use_thy "Dagstuhl";
+time_use_thy "Focus_ex";
 
+cd "..";
 maketest "END: Root file for HOLCF examples: explicit domain axiomatization";
diff -r 5bf4a54ba25f -r 4a960c012383 src/ZF/AC/ROOT.ML
--- a/src/ZF/AC/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/ZF/AC/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -11,35 +11,31 @@
 writeln"Root file for ZF/AC";
 proof_timing := true;
 
-loadpath := [".", "AC"];
-
-time_use_thy "AC/AC_Equiv";
+time_use_thy "AC_Equiv";
 
-time_use     "AC/WO1_WO6.ML";
-time_use_thy "AC/WO6_WO1";
-time_use     "AC/WO1_WO7.ML";
-time_use     "AC/WO1_WO8.ML";
+time_use     "WO1_WO6.ML";
+time_use_thy "WO6_WO1";
+time_use     "WO1_WO7.ML";
+time_use     "WO1_WO8.ML";
 
-time_use     "AC/AC0_AC1.ML";
-time_use     "AC/AC2_AC6.ML";
-time_use     "AC/AC7_AC9.ML";
+time_use     "AC0_AC1.ML";
+time_use     "AC2_AC6.ML";
+time_use     "AC7_AC9.ML";
 
-time_use_thy "AC/WO1_AC";
-time_use_thy "AC/AC1_WO2";
+time_use_thy "WO1_AC";
+time_use_thy "AC1_WO2";
 
-time_use     "AC/AC10_AC15.ML";
-time_use_thy "AC/AC15_WO6";
-
-time_use_thy "AC/WO2_AC16";
-time_use_thy "AC/AC16_WO4";
+time_use     "AC10_AC15.ML";
+time_use_thy "AC15_WO6";
 
-time_use     "AC/AC1_AC17.ML";
-time_use_thy "AC/AC17_AC1";
+time_use_thy "WO2_AC16";
+time_use_thy "AC16_WO4";
 
-time_use_thy "AC/AC18_AC19";
+time_use     "AC1_AC17.ML";
+time_use_thy "AC17_AC1";
 
-time_use_thy "AC/DC";
+time_use_thy "AC18_AC19";
 
-make_chart ();   (*make HTML chart*)
+time_use_thy "DC";
 
 writeln"END: Root file for ZF/AC";
diff -r 5bf4a54ba25f -r 4a960c012383 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/ZF/Coind/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -17,7 +17,5 @@
 
 writeln"Root file for ZF/Coind";
 proof_timing := true;
-loadpath     := [".","Coind"];
+
 time_use_thy "MT";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/ZF/IMP/ROOT.ML
--- a/src/ZF/IMP/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/ZF/IMP/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -16,7 +16,5 @@
 
 writeln"Root file for ZF/IMP";
 proof_timing := true;
-loadpath := [".","IMP"];
+
 time_use_thy "Equiv";
-
-make_chart ();   (*make HTML chart*)
diff -r 5bf4a54ba25f -r 4a960c012383 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/ZF/Resid/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -17,10 +17,6 @@
 writeln"Root file for ZF/Resid";
 proof_timing := true;
 
-loadpath := [".", "Resid"];
-
 time_use_thy "Confluence";
 
-make_chart ();   (*make HTML chart*)
-
 writeln"END: Root file for ZF/Resid";
diff -r 5bf4a54ba25f -r 4a960c012383 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/ZF/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -11,37 +11,33 @@
 writeln"Root file for ZF Set Theory examples";
 proof_timing := true;
 
-loadpath := [".", "ex"];
-
-time_use     "ex/misc.ML";
-time_use_thy "ex/Ramsey";
-time_use_thy "ex/Limit";
+time_use     "misc.ML";
+time_use_thy "Ramsey";
+time_use_thy "Limit";
 
 (*Integers & Binary integer arithmetic*)
-time_use_thy "ex/Bin";
+time_use_thy "Bin";
 
 (** Datatypes **)
-time_use_thy "ex/BT";		(*binary trees*)
-time_use_thy "ex/Data";		(*Sample datatype*)
-time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
-time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
-time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
-time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
-time_use_thy "ex/Enum";		(*Enormous enumeration type*)
+time_use_thy "BT";		(*binary trees*)
+time_use_thy "Data";		(*Sample datatype*)
+time_use_thy "Term";		(*terms: recursion over the list functor*)
+time_use_thy "TF";		(*trees/forests: mutual recursion*)
+time_use_thy "Ntree";		(*variable-branching trees; function demo*)
+time_use_thy "Brouwer";		(*Infinite-branching trees*)
+time_use_thy "Enum";		(*Enormous enumeration type*)
 
 (** Inductive definitions **)
-time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
-time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
+time_use_thy "Rmap";		(*mapping a relation over a list*)
+time_use_thy "PropLog";		(*completeness of propositional logic*)
 (*two Coq examples by Christine Paulin-Mohring*)
-time_use_thy "ex/ListN";
-time_use_thy "ex/Acc";
-time_use_thy "ex/Comb";		(*Combinatory Logic example*)
-time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
+time_use_thy "ListN";
+time_use_thy "Acc";
+time_use_thy "Comb";		(*Combinatory Logic example*)
+time_use_thy "Primrec";		(*Primitive recursive functions*)
 
 (** CoDatatypes **)
-time_use_thy "ex/LList";
-time_use_thy "ex/CoUnit";
-
-make_chart ();   (*make HTML chart*)
+time_use_thy "LList";
+time_use_thy "CoUnit";
 
 writeln"END: Root file for ZF Set Theory examples";