# HG changeset patch
# User clasohm
# Date 752418719 -3600
# Node ID a90653dabebcbe242627c5d304d5ac8d08efc1db
# Parent  2fee1120cb3e160f69d7f2c0b93f9a824f89a117
renamed some files

diff -r 2fee1120cb3e -r a90653dabebc src/ZF/Makefile
--- a/src/ZF/Makefile	Thu Nov 04 10:34:49 1993 +0100
+++ b/src/ZF/Makefile	Thu Nov 04 14:11:59 1993 +0100
@@ -21,7 +21,7 @@
 FILES = ROOT.ML zf.thy zf.ML upair.ML subset.ML pair.ML domrange.ML \
 	func.ML simpdata.ML bool.thy bool.ML \
 	sum.thy sum.ML qpair.thy qpair.ML mono.ML fixedpt.thy fixedpt.ML \
-	ind-syntax.ML intr-elim.ML indrule.ML inductive.ML co-inductive.ML \
+	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML co_inductive.ML \
 	equalities.ML perm.thy perm.ML trancl.thy trancl.ML \
 	wf.thy wf.ML ord.thy ord.ML nat.thy nat.ML \
 	epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \
diff -r 2fee1120cb3e -r a90653dabebc src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Nov 04 10:34:49 1993 +0100
+++ b/src/ZF/ROOT.ML	Thu Nov 04 14:11:59 1993 +0100
@@ -47,11 +47,11 @@
 use_thy "fixedpt";
 
 (*Inductive/co-inductive definitions*)
-use     "ind-syntax.ML";
-use     "intr-elim.ML";
+use     "ind_syntax.ML";
+use     "intr_elim.ML";
 use     "indrule.ML";
 use     "inductive.ML";
-use     "co-inductive.ML";
+use     "coinductive.ML";
 
 use_thy "perm";
 use_thy "trancl";