--- 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 \
--- 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";