removed make_chart;
theories are now read from the current directory (because of use_dir)
--- 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";
--- 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";
--- 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";
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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*)
--- 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*)
--- 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";
--- 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";