--- a/src/ZF/ex/ROOT.ML Tue Nov 16 14:24:21 1993 +0100
+++ b/src/ZF/ex/ROOT.ML Tue Nov 16 14:26:15 1993 +0100
@@ -11,27 +11,29 @@
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/Ramsey";
(*Equivalence classes and integers*)
-time_use_thy "ex/equiv";
-time_use_thy "ex/integ";
+time_use_thy "ex/Equiv";
+time_use_thy "ex/Integ";
(*Binary integer arithmetic*)
use "ex/twos_compl.ML";
time_use "ex/bin.ML";
-time_use_thy "ex/binfn";
+time_use_thy "ex/BinFn";
(** Datatypes **)
(*binary trees*)
time_use "ex/bt.ML";
-time_use_thy "ex/bt_fn";
+time_use_thy "ex/BT_Fn";
(*terms: recursion over the list functor*)
time_use "ex/term.ML";
-time_use_thy "ex/termfn";
+time_use_thy "ex/TermFn";
(*trees/forests: mutual recursion*)
time_use "ex/tf.ML";
-time_use_thy "ex/tf_fn";
+time_use_thy "ex/TF_Fn";
(*Sample datatype; enormous enumeration type*)
time_use "ex/data.ML";
time_use "ex/enum.ML";
@@ -41,20 +43,20 @@
time_use "ex/rmap.ML";
(*completeness of propositional logic*)
time_use "ex/prop.ML";
-time_use_thy "ex/proplog";
+time_use_thy "ex/PropLog";
(*two Coq examples by Ch. Paulin-Mohring*)
time_use "ex/listn.ML";
time_use "ex/acc.ML";
(*Diamond property for combinatory logic*)
time_use "ex/comb.ML";
-time_use_thy "ex/contract0";
+time_use_thy "ex/Contract0";
time_use "ex/parcontract.ML";
-time_use_thy "ex/primrec0";
+time_use_thy "ex/Primrec0";
(** CoDatatypes **)
time_use_thy "ex/LList";
time_use "ex/llist_eq.ML";
-time_use_thy "ex/llistfn";
+time_use_thy "ex/LListFn";
time_use "ex/counit.ML";
maketest"END: Root file for ZF Set Theory examples";