src/ZF/ROOT.ML
changeset 90 a90653dabebc
parent 75 144ec40f2650
child 120 09287f26bfb8
--- 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";