src/ZF/ex/ROOT.ML
changeset 1351 4a960c012383
parent 1296 ae31bb7774a7
child 1461 6bcb44e4d6e5
--- 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";