# HG changeset patch
# User clasohm
# Date 751293867 -3600
# Node ID c616d66c640e0e36cd3336761ea895a277c3afb3
# Parent  144ec40f2650d3d507a19714be6219a366a44ecc
renamed some files

diff -r 144ec40f2650 -r c616d66c640e src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Fri Oct 22 13:43:45 1993 +0100
+++ b/src/ZF/ex/ROOT.ML	Fri Oct 22 13:44:27 1993 +0100
@@ -41,18 +41,18 @@
 time_use     "ex/rmap.ML";
 (*completeness of propositional logic*)
 time_use     "ex/prop.ML";
-time_use_thy "ex/propthms";
+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/contract";
+time_use_thy "ex/contract0";
 time_use     "ex/parcontract.ML";
-time_use_thy "ex/primrec";
+time_use_thy "ex/primrec0";
 
 (** Co-Datatypes **)
-time_use     "ex/llist.ML";
+time_use_thy "ex/LList";
 time_use     "ex/llist_eq.ML";
 time_use_thy "ex/llistfn";