# HG changeset patch
# User clasohm
# Date 753456375 -3600
# Node ID bba27d15d76e152ac1a0330a6085df0b900d5f86
# Parent  858ab9a9b04720afbad3c1cbafbea6eda2b28b92
changed use_thy's parameter to exact theory name

diff -r 858ab9a9b047 -r bba27d15d76e src/ZF/ex/ROOT.ML
--- 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";